Theorem r19.41v 3162

Description: Restricted quantifier version 19.41v 1950. Version of r19.41 3236 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 3057	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1849	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1950	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3057	. . . 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 1780   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  r19.42v  3164  r19.41vv  3202  3reeanv  3205  reuxfr1d  3704  reuind  3707  iuncom4  4945  iunxiun  5040  inuni  5283  xpiundi  5682  xpiundir  5683  imaco  6193  coiun  6199  abrexco  7173  imaiun  7174  isomin  7266  isoini  7267  imaeqsexvOLD  7292  imaeqexov  7579  oarec  8472  mapsnend  8953  unfi  9075  brttrcl2  9599  genpass  10895  4fvwrd4  13543  4sqlem12  16863  imasleval  17440  lsmspsn  21013  utoptop  24144  metrest  24434  metust  24468  cfilucfil  24469  metuel2  24475  sleadd1  27927  addsuniflem  27939  addsasslem1  27941  addsasslem2  27942  addsdilem1  28085  0reno  28394  renegscl  28395  readdscl  28396  remulscl  28399  istrkg2ld  28433  axsegcon  28900  fusgreg2wsp  30308  nmoo0  30763  nmop0  31958  nmfn0  31959  rexunirn  32463  dmrab  32468  iunrnmptss  32537  ressupprn  32663  ordtconnlem1  33929  dya2icoseg2  34283  dya2iocnei  34287  omssubaddlem  34304  omssubadd  34305  r1omhf  35109  satfvsuclem2  35396  satf0  35408  satffunlem1lem2  35439  satffunlem2lem2  35442  rexxfr3dALT  35675  bj-mpomptALT  37153  mptsnunlem  37372  fvineqsneq  37446  rabiun  37633  iundif1  37634  poimir  37693  ismblfin  37701  eldmqs1cossres  38697  erimeq2  38716  prter2  38920  prter3  38921  islshpat  39056  lshpsmreu  39148  islpln5  39574  islvol5  39618  cdlemftr3  40604  dvhb1dimN  41025  dib1dim  41204  mapdpglem3  41714  hdmapglem7a  41966  diophrex  42808  dfsclnbgr6  47889  r19.41dv  48833  reuxfr1dd  48838