Theorem rspc2ev 3593

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 3580	. . . 4 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑦 ∈ 𝐷 𝜒)
3	2	anim2i 628	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ (𝐵 ∈ 𝐷 ∧ 𝜓)) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
4	3	3impb 1130	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → (𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒))
5		rspc2v.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
6	5	rexbidv 3187	. . 3 ⊢ (𝑥 = 𝐴 → (∃𝑦 ∈ 𝐷 𝜑 ↔ ∃𝑦 ∈ 𝐷 𝜒))
7	6	rspcev 3580	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ ∃𝑦 ∈ 𝐷 𝜒) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)
8	4, 7	syl 18	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝜓) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 𝜑)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088

This theorem is referenced by:  2rspcedvdw  3594  opelxp  5697  fprb  7192  f1prex  7282  nf1const  7302  rspceov  7459  erov  8811  ralxpmap  8893  2dom  9026  elfiun  9389  dffi3  9390  ixpiunwdom  9551  1re  11207  hashdmpropge2  14519  wrdl2exs2  14982  ello12r  15567  ello1d  15573  elo12r  15578  o1lo1  15587  addcn2  15644  mulcn2  15646  bezoutlem3  16598  bezout  16600  pythagtriplem18  16891  pczpre  16906  pcdiv  16911  4sqlem3  17009  4sqlem4  17011  4sqlem12  17015  vdwlem1  17040  vdwlem6  17045  vdwlem8  17047  vdwlem12  17051  vdwlem13  17052  0ram  17079  ramz2  17083  cat1lem  18152  sgrp2rid2ex  18988  pmtr3ncom  19544  psgnunilem1  19562  irredn0  20504  isnzr2  20600  hausnei2  23489  cnhaus  23490  dishaus  23518  ordthauslem  23519  txuni2  23701  xkoopn  23725  txopn  23738  txdis  23768  txdis1cn  23771  pthaus  23774  txhaus  23783  tx1stc  23786  xkohaus  23789  regr1lem  23875  qustgplem  24257  methaus  24656  met2ndci  24658  metnrmlem3  24998  elplyr  26337  aaliou2b  26481  aaliou3lem9  26490  2irrexpq  26872  2irrexpqALT  26941  2sqlem2  27558  2sqlem8  27566  2sqlem11  27569  2sqb  27572  2sqnn  27579  pntibnd  27733  madecut  28052  mulsproplem12  28296  precsexlem11  28386  eucliddivs  28545  elz12si  28642  zz12s  28644  remulscllem1  28669  legov  28830  iscgrad  29095  f1otrge  29187  axsegconlem1  29233  axsegcon  29243  axpaschlem  29256  axlowdimlem6  29263  axlowdim1  29275  axlowdim2  29276  axeuclidlem  29278  umgrvad2edg  29529  wwlksnwwlksnon  30230  upgr4cycl4dv4e  30502  3cyclfrgrrn1  30602  4cycl2vnunb  30607  br8d  32919  lt2addrd  33061  xlt2addrd  33070  xrnarchi  33470  txomap  34190  tpr2rico  34268  qqhval2  34338  elsx  34550  br2base  34625  dya2iocnrect  34637  connpconn  35681  satfv1fvfmla1  35869  br8  36202  br4  36204  brsegle  36554  hilbert1.1  36600  nn0prpwlem  36777  knoppndvlem21  37065  poimirlem1  38216  itg2addnclem3  38268  cntotbnd  38391  smprngopr  38647  3dim2  40188  llni2  40232  lvoli3  40297  lvoli2  40301  islinei  40460  psubspi2N  40468  elpaddri  40522  eldioph2lem1  43439  diophin  43451  fphpdo  43492  irrapxlem3  43499  irrapxlem4  43500  pellexlem6  43509  pell1234qrreccl  43529  pell1234qrmulcl  43530  pell1234qrdich  43536  pell1qr1  43546  pellqrexplicit  43552  rmxycomplete  43592  dgraalem  43820  tfsconcatrev  44023  clsk3nimkb  44714  fourierdlem64  46832  rspceaov  47879  modn0mul  48045  ichnreuop  48166  prelspr  48180  reuopreuprim  48220  6gbe  48481  7gbow  48482  8gbe  48483  9gbo  48484  11gbo  48485  smprngprmrng  49049  elbigo2r  49278  rrx2xpref1o  49443  inlinecirc02plem  49511  sepfsepc  49651  iscnrm3lem7  49662