Theorem r19.41v 3167

Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3241 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 3054	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1848	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1949	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3054	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 627	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.42v  3169  r19.41vv  3207  3reeanv  3210  reuxfr1d  3721  reuind  3724  iuncom4  4964  dfiun2gOLD  4995  iunxiun  5061  inuni  5305  xpiundi  5709  xpiundir  5710  imaco  6224  coiun  6229  abrexco  7218  imaiun  7219  isomin  7312  isoini  7313  imaeqsexvOLD  7338  imaeqexov  7627  oarec  8526  mapsnend  9007  unfi  9135  brttrcl2  9667  genpass  10962  4fvwrd4  13609  4sqlem12  16927  imasleval  17504  lsmspsn  20991  utoptop  24122  metrest  24412  metust  24446  cfilucfil  24447  metuel2  24453  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  addsdilem1  28054  0reno  28348  renegscl  28349  readdscl  28350  remulscl  28353  istrkg2ld  28387  axsegcon  28854  fusgreg2wsp  30265  nmoo0  30720  nmop0  31915  nmfn0  31916  rexunirn  32421  dmrab  32426  iunrnmptss  32494  ressupprn  32613  ordtconnlem1  33914  dya2icoseg2  34269  dya2iocnei  34273  omssubaddlem  34290  omssubadd  34291  satfvsuclem2  35347  satf0  35359  satffunlem1lem2  35390  satffunlem2lem2  35393  rexxfr3dALT  35626  bj-mpomptALT  37107  mptsnunlem  37326  fvineqsneq  37400  rabiun  37587  iundif1  37588  poimir  37647  ismblfin  37655  eldmqs1cossres  38651  erimeq2  38670  prter2  38874  prter3  38875  islshpat  39010  lshpsmreu  39102  islpln5  39529  islvol5  39573  cdlemftr3  40559  dvhb1dimN  40980  dib1dim  41159  mapdpglem3  41669  hdmapglem7a  41921  diophrex  42763  dfsclnbgr6  47858  r19.41dv  48790  reuxfr1dd  48795