Theorem r19.41v 3182

Description: Restricted quantifier version 19.41v 1959. Version of r19.41 3256 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 3077	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 471	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1858	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1959	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3077	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 226	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 635	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 301	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1789   ∈ wcel 2132  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-rex 3077

This theorem is referenced by:  r19.42v  3184  r19.41vv  3222  3reeanv  3225  reuxfr1d  3703  reuind  3706  iuncom4  4948  iunxiun  5044  inuni  5296  xpiundi  5707  xpiundir  5708  imaco  6223  coiun  6229  abrexco  7213  imaiun  7214  isomin  7306  isoini  7307  imaeqsexvOLD  7332  imaeqexov  7619  oarec  8515  mapsnend  9002  unfi  9124  brttrcl2  9655  genpass  10953  4fvwrd4  13639  4sqlem12  16964  imasleval  17543  lsmspsn  21120  utoptop  24263  metrest  24553  metust  24587  cfilucfil  24588  metuel2  24594  leadds1  28048  addsuniflem  28060  addsasslem1  28062  addsasslem2  28063  addsdilem1  28210  elreno2  28554  renegscl  28557  readdscl  28558  remulscl  28561  istrkg2ld  28595  axsegcon  29063  fusgreg2wsp  30473  nmoo0  30929  nmop0  32124  nmfn0  32125  rexunirn  32628  dmrab  32633  iunrnmptss  32703  ressupprn  32831  ordtconnlem1  34165  dya2icoseg2  34519  dya2iocnei  34523  omssubaddlem  34540  omssubadd  34541  r1omhf  35347  satfvsuclem2  35648  satf0  35660  satffunlem1lem2  35691  satffunlem2lem2  35694  rexxfr3dALT  35927  bj-mpomptALT  37547  mptsnunlem  37770  fvineqsneq  37844  rabiun  38030  iundif1  38031  poimir  38090  ismblfin  38098  eldmqs1cossres  39181  erimeq2  39200  prter2  39443  prter3  39444  islshpat  39579  lshpsmreu  39671  islpln5  40097  islvol5  40141  cdlemftr3  41127  dvhb1dimN  41548  dib1dim  41727  mapdpglem3  42237  hdmapglem7a  42489  diophrex  43294  dfsclnbgr6  48418  r19.41dv  49361  reuxfr1dd  49366