Theorem r19.41v 3196

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.42v  3198  r19.41vv  3236  3reeanv  3239  reuxfr1d  3711  reuind  3714  iuncom4  4965  iunxiun  5062  inuni  5318  xpiundi  5729  xpiundir  5730  imaco  6271  coiun  6277  abrexco  7279  imaiun  7280  isomin  7376  isoini  7377  imaeqexov  7691  mpt3mpt  7717  oarec  8608  mapsnend  9102  unfi  9224  brttrcl2  9752  genpass  11133  4fvwrd4  13822  4sqlem12  17178  imasleval  17763  lsmspsn  21410  utoptop  24608  metrest  24898  metust  24932  cfilucfil  24933  metuel2  24939  leadds1  28432  addsuniflem  28444  addsasslem1  28446  addsasslem2  28447  addsdilem1  28594  elreno2  28938  renegscl  28941  readdscl  28942  remulscl  28945  istrkg2ld  28979  axsegcon  29562  fusgreg2wsp  30994  nmoo0  31450  nmop0  32645  nmfn0  32646  rexunirn  33187  dmrab  33192  iunrnmptss  33257  ressupprn  33380  ordtconnlem1  34667  dya2icoseg2  35021  dya2iocnei  35025  omssubaddlem  35042  omssubadd  35043  vonf1oonfo  36090  satfvsuclem2  36333  satf0  36345  satffunlem1lem2  36376  satffunlem2lem2  36379  rexxfr3dALT  36612  mirimanofffr  36670  bj-mpomptALT  38311  mptsnunlem  38529  fvineqsneq  38603  rabiun  38789  iundif1  38790  poimir  38839  ismblfin  38847  eldmqs1cossres  39942  erimeq2  39961  prter2  40204  prter3  40205  islshpat  40340  lshpsmreu  40432  islpln5  40858  islvol5  40902  cdlemftr3  41888  dvhb1dimN  42309  dib1dim  42488  mapdpglem3  42998  hdmapglem7a  43250  diophrex  44052  dfsclnbgr6  49229  r19.41dv  50243  reuxfr1dd  50248