Theorem rspc2ev 3625

Description: 2-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 16-Oct-1999.)

Hypotheses

Ref	Expression
rspc2v.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
rspc2v.2	⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))

Assertion

Ref	Expression
rspc2ev	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2ev

Step	Hyp	Ref	Expression
1		rspc2v.2	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓))
2	1	rspcev 3613	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 618	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1116	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3179	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3613	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 17	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∃wrex 3071

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  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072

This theorem is referenced by:  2rspcedvdw  3626  rspc3ev  3629  opelxp  5713  fprb  7195  f1prex  7282  nf1const  7302  rspceov  7456  erov  8808  ralxpmap  8890  2dom  9030  elfiun  9425  dffi3  9426  ixpiunwdom  9585  1re  11214  hashdmpropge2  14444  wrdl2exs2  14897  ello12r  15461  ello1d  15467  elo12r  15472  o1lo1  15481  addcn2  15538  mulcn2  15540  bezoutlem3  16483  bezout  16485  pythagtriplem18  16765  pczpre  16780  pcdiv  16785  4sqlem3  16883  4sqlem4  16885  4sqlem12  16889  vdwlem1  16914  vdwlem6  16919  vdwlem8  16921  vdwlem12  16925  vdwlem13  16926  0ram  16953  ramz2  16957  cat1lem  18046  sgrp2rid2ex  18808  pmtr3ncom  19343  psgnunilem1  19361  irredn0  20237  isnzr2  20297  hausnei2  22857  cnhaus  22858  dishaus  22886  ordthauslem  22887  txuni2  23069  xkoopn  23093  txopn  23106  txdis  23136  txdis1cn  23139  pthaus  23142  txhaus  23151  tx1stc  23154  xkohaus  23157  regr1lem  23243  qustgplem  23625  methaus  24029  met2ndci  24031  metnrmlem3  24377  elplyr  25715  aaliou2b  25854  aaliou3lem9  25863  2irrexpq  26239  2irrexpqALT  26305  2sqlem2  26921  2sqlem8  26929  2sqlem11  26932  2sqb  26935  2sqnn0  26941  2sqnn  26942  pntibnd  27096  madecut  27378  mulsproplem12  27586  precsexlem11  27666  legov  27867  iscgrad  28093  f1otrge  28154  axsegconlem1  28206  axsegcon  28216  axpaschlem  28229  axlowdimlem6  28236  axlowdim1  28248  axlowdim2  28249  axeuclidlem  28251  umgrvad2edg  28501  wwlksnwwlksnon  29200  upgr4cycl4dv4e  29469  3cyclfrgrrn1  29569  4cycl2vnunb  29574  br8d  31870  lt2addrd  31995  xlt2addrd  32002  xrnarchi  32361  txomap  32845  tpr2rico  32923  qqhval2  32993  elsx  33223  br2base  33299  dya2iocnrect  33311  connpconn  34257  satfv1fvfmla1  34445  br8  34757  br4  34759  brsegle  35111  hilbert1.1  35157  nn0prpwlem  35255  knoppndvlem21  35456  poimirlem1  36537  itg2addnclem3  36589  cntotbnd  36712  smprngopr  36968  3dim2  38387  llni2  38431  lvoli3  38496  lvoli2  38500  islinei  38659  psubspi2N  38667  elpaddri  38721  eldioph2lem1  41546  diophin  41558  fphpdo  41603  irrapxlem3  41610  irrapxlem4  41611  pellexlem6  41620  pell1234qrreccl  41640  pell1234qrmulcl  41641  pell1234qrdich  41647  pell1qr1  41657  pellqrexplicit  41663  rmxycomplete  41704  dgraalem  41935  tfsconcatrev  42146  clsk3nimkb  42839  fourierdlem64  44934  rspceaov  45953  ichnreuop  46188  prelspr  46202  reuopreuprim  46242  6gbe  46487  7gbow  46488  8gbe  46489  9gbo  46490  11gbo  46491  modn0mul  47254  elbigo2r  47287  rrx2xpref1o  47452  inlinecirc02plem  47520  sepfsepc  47608  iscnrm3lem7  47620