Theorem r19.29r 3112

Description: Restricted quantifier version of 19.29r 1870; variation of r19.29 3110. (Contributed by NM, 31-Aug-1999.) (Proof shortened by Wolf Lammen, 29-Jun-2023.)

Assertion

Ref	Expression
r19.29r	⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Proof of Theorem r19.29r

Step	Hyp	Ref	Expression
1		iba 527	. . 3 ⊢ (𝜓 → (𝜑 ↔ (𝜑 ∧ 𝜓)))
2	1	ralrexbid 3102	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓)))
3	2	biimpac 478	1 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 𝜓) → ∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395  ∀wral 3057  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-ral 3058  df-rex 3067

This theorem is referenced by:  r19.29imd  3114  2reu5  3752  rlimuni  15520  rlimno1  15626  neindisj2  23020  lmss  23195  fclsbas  23918  isfcf  23931  ucnima  24179  metcnp3  24442  cfilucfil  24461  bndth  24877  ellimc3  25801  lmxrge0  33547  gsumesum  33672  esumcst  33676  esumfsup  33683  voliune  33842  volfiniune  33843  bnj517  34510  nummin  34708  fvineqsneq  36885  cover2  37182  naddgeoa  42818  prmunb2  43742

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »