Theorem r19.41v 3193

Description: Restricted quantifier version 19.41v 1982. Version of r19.41 3267 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)

Assertion

Ref	Expression
r19.41v	⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		df-rex 3088	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 474	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1881	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1982	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3088	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 227	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 639	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  r19.42v  3195  r19.41vv  3233  3reeanv  3236  reuxfr1d  3708  reuind  3711  iuncom4  4960  iunxiun  5057  inuni  5311  xpiundi  5722  xpiundir  5723  imaco  6251  coiun  6257  abrexco  7246  imaiun  7247  isomin  7343  isoini  7344  imaeqexov  7657  mpt3mpt  7683  oarec  8563  mapsnend  9057  unfi  9179  brttrcl2  9708  genpass  11087  4fvwrd4  13775  4sqlem12  17127  imasleval  17706  lsmspsn  21352  utoptop  24546  metrest  24836  metust  24870  cfilucfil  24871  metuel2  24877  leadds1  28368  addsuniflem  28380  addsasslem1  28382  addsasslem2  28383  addsdilem1  28530  elreno2  28874  renegscl  28877  readdscl  28878  remulscl  28881  istrkg2ld  28915  axsegcon  29498  fusgreg2wsp  30930  nmoo0  31386  nmop0  32581  nmfn0  32582  rexunirn  33081  dmrab  33086  iunrnmptss  33152  ressupprn  33276  ordtconnlem1  34549  dya2icoseg2  34903  dya2iocnei  34907  omssubaddlem  34924  omssubadd  34925  vonf1oonfo  35877  satfvsuclem2  36104  satf0  36116  satffunlem1lem2  36147  satffunlem2lem2  36150  rexxfr3dALT  36383  bj-mpomptALT  38020  mptsnunlem  38241  fvineqsneq  38315  rabiun  38501  iundif1  38502  poimir  38551  ismblfin  38559  eldmqs1cossres  39656  erimeq2  39675  prter2  39918  prter3  39919  islshpat  40054  lshpsmreu  40146  islpln5  40572  islvol5  40616  cdlemftr3  41602  dvhb1dimN  42023  dib1dim  42202  mapdpglem3  42712  hdmapglem7a  42964  diophrex  43765  dfsclnbgr6  48925  r19.41dv  49881  reuxfr1dd  49886