Theorem r19.41v 3159

Description: Restricted quantifier version 19.41v 1949. Version of r19.41 3233 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  3161  r19.41vv  3199  3reeanv  3202  reuxfr1d  3712  reuind  3715  iuncom4  4953  iunxiun  5049  inuni  5292  xpiundi  5694  xpiundir  5695  imaco  6204  coiun  6209  abrexco  7184  imaiun  7185  isomin  7278  isoini  7279  imaeqsexvOLD  7304  imaeqexov  7591  oarec  8487  mapsnend  8968  unfi  9095  brttrcl2  9629  genpass  10922  4fvwrd4  13570  4sqlem12  16887  imasleval  17464  lsmspsn  21007  utoptop  24139  metrest  24429  metust  24463  cfilucfil  24464  metuel2  24470  sleadd1  27920  addsuniflem  27932  addsasslem1  27934  addsasslem2  27935  addsdilem1  28078  0reno  28385  renegscl  28386  readdscl  28387  remulscl  28390  istrkg2ld  28424  axsegcon  28891  fusgreg2wsp  30299  nmoo0  30754  nmop0  31949  nmfn0  31950  rexunirn  32455  dmrab  32460  iunrnmptss  32528  ressupprn  32651  ordtconnlem1  33910  dya2icoseg2  34265  dya2iocnei  34269  omssubaddlem  34286  omssubadd  34287  satfvsuclem2  35352  satf0  35364  satffunlem1lem2  35395  satffunlem2lem2  35398  rexxfr3dALT  35631  bj-mpomptALT  37112  mptsnunlem  37331  fvineqsneq  37405  rabiun  37592  iundif1  37593  poimir  37652  ismblfin  37660  eldmqs1cossres  38656  erimeq2  38675  prter2  38879  prter3  38880  islshpat  39015  lshpsmreu  39107  islpln5  39534  islvol5  39578  cdlemftr3  40564  dvhb1dimN  40985  dib1dim  41164  mapdpglem3  41674  hdmapglem7a  41926  diophrex  42768  dfsclnbgr6  47862  r19.41dv  48806  reuxfr1dd  48811