Theorem r19.41v 3181

Description: Restricted quantifier version 19.41v 1952. Version of r19.41 3242 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		anass 469	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1849	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1952	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 276	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 624	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1780   ∈ wcel 2105  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3071

This theorem is referenced by:  r19.42v  3183  r19.41vv  3211  3reeanv  3214  reuxfr1d  3696  reuind  3699  iuncom4  4949  dfiun2gOLD  4978  iunxiun  5044  inuni  5287  xpiundi  5688  xpiundir  5689  imaco  6189  coiun  6194  abrexco  7173  imaiun  7174  isomin  7264  isoini  7265  oarec  8464  mapsnend  8901  unfi  9037  brttrcl2  9571  genpass  10866  4fvwrd4  13477  4sqlem12  16754  imasleval  17349  lsmspsn  20452  utoptop  23492  metrest  23786  metust  23820  cfilucfil  23821  metuel2  23827  istrkg2ld  27110  axsegcon  27584  fusgreg2wsp  28988  nmoo0  29441  nmop0  30636  nmfn0  30637  rexunirn  31128  dmrab  31132  iunrnmptss  31192  ressupprn  31311  ordtconnlem1  32172  dya2icoseg2  32545  dya2iocnei  32549  omssubaddlem  32566  omssubadd  32567  satfvsuclem2  33621  satf0  33633  satffunlem1lem2  33664  satffunlem2lem2  33667  imaeqsexv  33980  bj-mpomptALT  35403  mptsnunlem  35622  fvineqsneq  35696  rabiun  35863  iundif1  35864  poimir  35923  ismblfin  35931  eldmqs1cossres  36934  erimeq2  36953  prter2  37156  prter3  37157  islshpat  37292  lshpsmreu  37384  islpln5  37811  islvol5  37855  cdlemftr3  38841  dvhb1dimN  39262  dib1dim  39441  mapdpglem3  39951  hdmapglem7a  40203  diophrex  40867  r19.41dv  46507