Theorem r19.41v 3163

Description: Restricted quantifier version 19.41v 1950. Version of r19.41 3237 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 3058	. 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
2		anass 468	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
3	2	exbii 1849	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)))
4		19.41v 1950	. . 3 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓))
5		df-rex 3058	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6	5	bicomi 224	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
7	4, 6	bianbi 627	. 2 ⊢ (∃𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))
8	1, 3, 7	3bitr2i 299	1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3058

This theorem is referenced by:  r19.42v  3165  r19.41vv  3203  3reeanv  3206  reuxfr1d  3705  reuind  3708  iuncom4  4952  iunxiun  5049  inuni  5292  xpiundi  5692  xpiundir  5693  imaco  6206  coiun  6212  abrexco  7187  imaiun  7188  isomin  7280  isoini  7281  imaeqsexvOLD  7306  imaeqexov  7593  oarec  8486  mapsnend  8969  unfi  9091  brttrcl2  9615  genpass  10911  4fvwrd4  13555  4sqlem12  16875  imasleval  17453  lsmspsn  21027  utoptop  24169  metrest  24459  metust  24493  cfilucfil  24494  metuel2  24500  sleadd1  27952  addsuniflem  27964  addsasslem1  27966  addsasslem2  27967  addsdilem1  28110  0reno  28419  renegscl  28420  readdscl  28421  remulscl  28424  istrkg2ld  28458  axsegcon  28926  fusgreg2wsp  30337  nmoo0  30792  nmop0  31987  nmfn0  31988  rexunirn  32492  dmrab  32497  iunrnmptss  32566  ressupprn  32695  ordtconnlem1  34009  dya2icoseg2  34363  dya2iocnei  34367  omssubaddlem  34384  omssubadd  34385  r1omhf  35189  satfvsuclem2  35476  satf0  35488  satffunlem1lem2  35519  satffunlem2lem2  35522  rexxfr3dALT  35755  bj-mpomptALT  37236  mptsnunlem  37455  fvineqsneq  37529  rabiun  37706  iundif1  37707  poimir  37766  ismblfin  37774  eldmqs1cossres  38830  erimeq2  38849  prter2  39053  prter3  39054  islshpat  39189  lshpsmreu  39281  islpln5  39707  islvol5  39751  cdlemftr3  40737  dvhb1dimN  41158  dib1dim  41337  mapdpglem3  41847  hdmapglem7a  42099  diophrex  42932  dfsclnbgr6  48020  r19.41dv  48963  reuxfr1dd  48968