Theorem r19.41v 3168

Description: Restricted quantifier version 19.41v 1949. 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		df-rex 3055	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1848	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1949	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3055	. . . 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 3054

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 3055

This theorem is referenced by:  r19.42v  3170  r19.41vv  3208  3reeanv  3211  reuxfr1d  3724  reuind  3727  iuncom4  4967  dfiun2gOLD  4998  iunxiun  5064  inuni  5308  xpiundi  5712  xpiundir  5713  imaco  6227  coiun  6232  abrexco  7221  imaiun  7222  isomin  7315  isoini  7316  imaeqsexvOLD  7341  imaeqexov  7630  oarec  8529  mapsnend  9010  unfi  9141  brttrcl2  9674  genpass  10969  4fvwrd4  13616  4sqlem12  16934  imasleval  17511  lsmspsn  20998  utoptop  24129  metrest  24419  metust  24453  cfilucfil  24454  metuel2  24460  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  addsdilem1  28061  0reno  28355  renegscl  28356  readdscl  28357  remulscl  28360  istrkg2ld  28394  axsegcon  28861  fusgreg2wsp  30272  nmoo0  30727  nmop0  31922  nmfn0  31923  rexunirn  32428  dmrab  32433  iunrnmptss  32501  ressupprn  32620  ordtconnlem1  33921  dya2icoseg2  34276  dya2iocnei  34280  omssubaddlem  34297  omssubadd  34298  satfvsuclem2  35354  satf0  35366  satffunlem1lem2  35397  satffunlem2lem2  35400  rexxfr3dALT  35633  bj-mpomptALT  37114  mptsnunlem  37333  fvineqsneq  37407  rabiun  37594  iundif1  37595  poimir  37654  ismblfin  37662  eldmqs1cossres  38658  erimeq2  38677  prter2  38881  prter3  38882  islshpat  39017  lshpsmreu  39109  islpln5  39536  islvol5  39580  cdlemftr3  40566  dvhb1dimN  40987  dib1dim  41166  mapdpglem3  41676  hdmapglem7a  41928  diophrex  42770  dfsclnbgr6  47862  r19.41dv  48794  reuxfr1dd  48799