Theorem r19.41v 3181

Description: Restricted quantifier version 19.41v 1953. Version of r19.41 3244 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 1850	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3		19.41v 1953	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
4	2, 3	bitr3i 276	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
6		df-rex 3070	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	anbi1i 624	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
8	4, 5, 7	3bitr4i 302	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  r19.42v  3183  r19.41vv  3213  3reeanv  3216  reuxfr1d  3711  reuind  3714  iuncom4  4967  dfiun2gOLD  4996  iunxiun  5062  inuni  5305  xpiundi  5707  xpiundir  5708  imaco  6208  coiun  6213  abrexco  7196  imaiun  7197  isomin  7287  isoini  7288  imaeqsexv  7313  imaeqexov  7597  oarec  8514  mapsnend  8987  unfi  9123  brttrcl2  9659  genpass  10954  4fvwrd4  13571  4sqlem12  16839  imasleval  17437  lsmspsn  20602  utoptop  23623  metrest  23917  metust  23951  cfilucfil  23952  metuel2  23958  sleadd1  27341  addsunif  27353  addsasslem1  27354  addsasslem2  27355  istrkg2ld  27465  axsegcon  27939  fusgreg2wsp  29343  nmoo0  29796  nmop0  30991  nmfn0  30992  rexunirn  31484  dmrab  31489  iunrnmptss  31551  ressupprn  31672  ordtconnlem1  32594  dya2icoseg2  32967  dya2iocnei  32971  omssubaddlem  32988  omssubadd  32989  satfvsuclem2  34041  satf0  34053  satffunlem1lem2  34084  satffunlem2lem2  34087  bj-mpomptALT  35663  mptsnunlem  35882  fvineqsneq  35956  rabiun  36124  iundif1  36125  poimir  36184  ismblfin  36192  eldmqs1cossres  37194  erimeq2  37213  prter2  37416  prter3  37417  islshpat  37552  lshpsmreu  37644  islpln5  38071  islvol5  38115  cdlemftr3  39101  dvhb1dimN  39522  dib1dim  39701  mapdpglem3  40211  hdmapglem7a  40463  diophrex  41156  r19.41dv  47007