Theorem r19.41v 3165

Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3239 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  3167  r19.41vv  3205  3reeanv  3208  reuxfr1d  3718  reuind  3721  iuncom4  4960  iunxiun  5056  inuni  5300  xpiundi  5702  xpiundir  5703  imaco  6212  coiun  6217  abrexco  7200  imaiun  7201  isomin  7294  isoini  7295  imaeqsexvOLD  7320  imaeqexov  7607  oarec  8503  mapsnend  8984  unfi  9112  brttrcl2  9643  genpass  10938  4fvwrd4  13585  4sqlem12  16903  imasleval  17480  lsmspsn  20967  utoptop  24098  metrest  24388  metust  24422  cfilucfil  24423  metuel2  24429  sleadd1  27872  addsuniflem  27884  addsasslem1  27886  addsasslem2  27887  addsdilem1  28030  0reno  28324  renegscl  28325  readdscl  28326  remulscl  28329  istrkg2ld  28363  axsegcon  28830  fusgreg2wsp  30238  nmoo0  30693  nmop0  31888  nmfn0  31889  rexunirn  32394  dmrab  32399  iunrnmptss  32467  ressupprn  32586  ordtconnlem1  33887  dya2icoseg2  34242  dya2iocnei  34246  omssubaddlem  34263  omssubadd  34264  satfvsuclem2  35320  satf0  35332  satffunlem1lem2  35363  satffunlem2lem2  35366  rexxfr3dALT  35599  bj-mpomptALT  37080  mptsnunlem  37299  fvineqsneq  37373  rabiun  37560  iundif1  37561  poimir  37620  ismblfin  37628  eldmqs1cossres  38624  erimeq2  38643  prter2  38847  prter3  38848  islshpat  38983  lshpsmreu  39075  islpln5  39502  islvol5  39546  cdlemftr3  40532  dvhb1dimN  40953  dib1dim  41132  mapdpglem3  41642  hdmapglem7a  41894  diophrex  42736  dfsclnbgr6  47831  r19.41dv  48763  reuxfr1dd  48768