Theorem r19.41v 3201

Description: Restricted quantifier version 19.41v 1976. Version of r19.41 3275 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 3096	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 473	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1875	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1976	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3096	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 227	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 638	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  r19.42v  3203  r19.41vv  3241  3reeanv  3244  reuxfr1d  3722  reuind  3725  iuncom4  4966  iunxiun  5064  inuni  5318  xpiundi  5730  xpiundir  5731  imaco  6249  coiun  6255  abrexco  7240  imaiun  7241  isomin  7333  isoini  7334  imaeqsexvOLD  7359  imaeqexov  7646  oarec  8543  mapsnend  9029  unfi  9151  brttrcl2  9679  genpass  10990  4fvwrd4  13672  4sqlem12  17012  imasleval  17591  lsmspsn  21179  utoptop  24356  metrest  24646  metust  24680  cfilucfil  24681  metuel2  24687  leadds1  28144  addsuniflem  28156  addsasslem1  28158  addsasslem2  28159  addsdilem1  28306  elreno2  28650  renegscl  28653  readdscl  28654  remulscl  28657  istrkg2ld  28691  axsegcon  29214  fusgreg2wsp  30624  nmoo0  31080  nmop0  32275  nmfn0  32276  rexunirn  32775  dmrab  32780  iunrnmptss  32847  ressupprn  32972  ordtconnlem1  34255  dya2icoseg2  34609  dya2iocnei  34613  omssubaddlem  34630  omssubadd  34631  r1omhf  35438  vonf1oonfo  35494  satfvsuclem2  35747  satf0  35759  satffunlem1lem2  35790  satffunlem2lem2  35793  rexxfr3dALT  36026  bj-mpomptALT  37644  mptsnunlem  37867  fvineqsneq  37941  rabiun  38127  iundif1  38128  poimir  38187  ismblfin  38195  eldmqs1cossres  39278  erimeq2  39297  prter2  39540  prter3  39541  islshpat  39676  lshpsmreu  39768  islpln5  40194  islvol5  40238  cdlemftr3  41224  dvhb1dimN  41645  dib1dim  41824  mapdpglem3  42334  hdmapglem7a  42586  diophrex  43391  dfsclnbgr6  48505  r19.41dv  49458  reuxfr1dd  49463