Theorem r19.41v 3189

Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3263 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 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1848	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1949	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3071	. . . 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 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  r19.42v  3191  r19.41vv  3227  3reeanv  3230  reuxfr1d  3756  reuind  3759  iuncom4  5000  dfiun2gOLD  5031  iunxiun  5097  inuni  5350  xpiundi  5756  xpiundir  5757  imaco  6271  coiun  6276  abrexco  7264  imaiun  7265  isomin  7357  isoini  7358  imaeqsexvOLD  7383  imaeqexov  7671  oarec  8600  mapsnend  9076  unfi  9211  brttrcl2  9754  genpass  11049  4fvwrd4  13688  4sqlem12  16994  imasleval  17586  lsmspsn  21083  utoptop  24243  metrest  24537  metust  24571  cfilucfil  24572  metuel2  24578  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  addsdilem1  28177  0reno  28429  renegscl  28430  readdscl  28431  remulscl  28434  istrkg2ld  28468  axsegcon  28942  fusgreg2wsp  30355  nmoo0  30810  nmop0  32005  nmfn0  32006  rexunirn  32511  dmrab  32516  iunrnmptss  32578  ressupprn  32699  ordtconnlem1  33923  dya2icoseg2  34280  dya2iocnei  34284  omssubaddlem  34301  omssubadd  34302  satfvsuclem2  35365  satf0  35377  satffunlem1lem2  35408  satffunlem2lem2  35411  rexxfr3dALT  35644  bj-mpomptALT  37120  mptsnunlem  37339  fvineqsneq  37413  rabiun  37600  iundif1  37601  poimir  37660  ismblfin  37668  eldmqs1cossres  38660  erimeq2  38679  prter2  38882  prter3  38883  islshpat  39018  lshpsmreu  39110  islpln5  39537  islvol5  39581  cdlemftr3  40567  dvhb1dimN  40988  dib1dim  41167  mapdpglem3  41677  hdmapglem7a  41929  diophrex  42786  dfsclnbgr6  47844  r19.41dv  48722  reuxfr1dd  48726