Theorem r19.41v 3277

Description: Restricted quantifier version 19.41v 1954. Version of r19.41 3278 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		anass 469	. . . 4 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2	1	exbii 1851	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1954	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 276	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 624	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 303	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  r19.41vv  3279  r19.42v  3280  3reeanv  3296  reuxfr1d  3686  reuind  3689  iuncom4  4933  dfiun2gOLD  4962  iunxiun  5027  inuni  5268  xpiundi  5658  xpiundir  5659  imaco  6159  coiun  6164  abrexco  7126  imaiun  7127  isomin  7217  isoini  7218  oarec  8402  mapsnend  8835  unfi  8964  brttrcl2  9481  genpass  10774  4fvwrd4  13385  4sqlem12  16666  imasleval  17261  lsmspsn  20355  utoptop  23395  metrest  23689  metust  23723  cfilucfil  23724  metuel2  23730  istrkg2ld  26830  axsegcon  27304  fusgreg2wsp  28709  nmoo0  29162  nmop0  30357  nmfn0  30358  rexunirn  30849  dmrab  30853  iunrnmptss  30914  ressupprn  31033  ordtconnlem1  31883  dya2icoseg2  32254  dya2iocnei  32258  omssubaddlem  32275  omssubadd  32276  satfvsuclem2  33331  satf0  33343  satffunlem1lem2  33374  satffunlem2lem2  33377  imaeqsexv  33699  bj-mpomptALT  35299  mptsnunlem  35518  fvineqsneq  35592  rabiun  35759  iundif1  35760  poimir  35819  ismblfin  35827  eldmqs1cossres  36778  erim2  36796  prter2  36902  prter3  36903  islshpat  37038  lshpsmreu  37130  islpln5  37556  islvol5  37600  cdlemftr3  38586  dvhb1dimN  39007  dib1dim  39186  mapdpglem3  39696  hdmapglem7a  39948  diophrex  40604  r19.41dv  46158