Theorem r19.41v 3178

Description: Restricted quantifier version 19.41v 1945. Version of r19.41 3250 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 3060	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 467	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1842	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1945	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3060	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 223	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 625	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 298	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  r19.42v  3180  r19.41vv  3214  3reeanv  3217  reuxfr1d  3742  reuind  3745  iuncom4  5005  dfiun2gOLD  5035  iunxiun  5101  inuni  5346  xpiundi  5748  xpiundir  5749  imaco  6257  coiun  6262  abrexco  7254  imaiun  7255  isomin  7344  isoini  7345  imaeqsexv  7370  imaeqexov  7659  oarec  8583  mapsnend  9061  unfi  9197  brttrcl2  9739  genpass  11034  4fvwrd4  13656  4sqlem12  16928  imasleval  17526  lsmspsn  20981  utoptop  24183  metrest  24477  metust  24511  cfilucfil  24512  metuel2  24518  sleadd1  27952  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  addsdilem1  28101  0reno  28297  renegscl  28298  readdscl  28299  remulscl  28302  istrkg2ld  28336  axsegcon  28810  fusgreg2wsp  30218  nmoo0  30673  nmop0  31868  nmfn0  31869  rexunirn  32368  dmrab  32373  iunrnmptss  32435  ressupprn  32552  ordtconnlem1  33656  dya2icoseg2  34029  dya2iocnei  34033  omssubaddlem  34050  omssubadd  34051  satfvsuclem2  35101  satf0  35113  satffunlem1lem2  35144  satffunlem2lem2  35147  bj-mpomptALT  36729  mptsnunlem  36948  fvineqsneq  37022  rabiun  37197  iundif1  37198  poimir  37257  ismblfin  37265  eldmqs1cossres  38261  erimeq2  38280  prter2  38483  prter3  38484  islshpat  38619  lshpsmreu  38711  islpln5  39138  islvol5  39182  cdlemftr3  40168  dvhb1dimN  40589  dib1dim  40768  mapdpglem3  41278  hdmapglem7a  41530  diophrex  42337  dfsclnbgr6  47330  r19.41dv  48060