Theorem rspc2ev 3614

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061

This theorem is referenced by:  2rspcedvdw  3615  rspc3ev  3618  opelxp  5690  fprb  7185  f1prex  7276  nf1const  7296  rspceov  7452  erov  8826  ralxpmap  8908  2dom  9042  elfiun  9440  dffi3  9441  ixpiunwdom  9602  1re  11233  hashdmpropge2  14499  wrdl2exs2  14963  ello12r  15531  ello1d  15537  elo12r  15542  o1lo1  15551  addcn2  15608  mulcn2  15610  bezoutlem3  16558  bezout  16560  pythagtriplem18  16850  pczpre  16865  pcdiv  16870  4sqlem3  16968  4sqlem4  16970  4sqlem12  16974  vdwlem1  16999  vdwlem6  17004  vdwlem8  17006  vdwlem12  17010  vdwlem13  17011  0ram  17038  ramz2  17042  cat1lem  18107  sgrp2rid2ex  18903  pmtr3ncom  19454  psgnunilem1  19472  irredn0  20381  isnzr2  20476  hausnei2  23289  cnhaus  23290  dishaus  23318  ordthauslem  23319  txuni2  23501  xkoopn  23525  txopn  23538  txdis  23568  txdis1cn  23571  pthaus  23574  txhaus  23583  tx1stc  23586  xkohaus  23589  regr1lem  23675  qustgplem  24057  methaus  24457  met2ndci  24459  metnrmlem3  24799  elplyr  26156  aaliou2b  26299  aaliou3lem9  26308  2irrexpq  26690  2irrexpqALT  26760  2sqlem2  27379  2sqlem8  27387  2sqlem11  27390  2sqb  27393  2sqnn0  27399  2sqnn  27400  pntibnd  27554  madecut  27838  mulsproplem12  28070  precsexlem11  28158  zzs12  28340  remulscllem1  28349  legov  28510  iscgrad  28736  f1otrge  28797  axsegconlem1  28842  axsegcon  28852  axpaschlem  28865  axlowdimlem6  28872  axlowdim1  28884  axlowdim2  28885  axeuclidlem  28887  umgrvad2edg  29138  wwlksnwwlksnon  29843  upgr4cycl4dv4e  30112  3cyclfrgrrn1  30212  4cycl2vnunb  30217  br8d  32536  lt2addrd  32674  xlt2addrd  32682  xrnarchi  33128  txomap  33811  tpr2rico  33889  qqhval2  33959  elsx  34171  br2base  34247  dya2iocnrect  34259  connpconn  35203  satfv1fvfmla1  35391  br8  35719  br4  35721  brsegle  36072  hilbert1.1  36118  nn0prpwlem  36286  knoppndvlem21  36496  poimirlem1  37591  itg2addnclem3  37643  cntotbnd  37766  smprngopr  38022  3dim2  39433  llni2  39477  lvoli3  39542  lvoli2  39546  islinei  39705  psubspi2N  39713  elpaddri  39767  eldioph2lem1  42730  diophin  42742  fphpdo  42787  irrapxlem3  42794  irrapxlem4  42795  pellexlem6  42804  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell1234qrdich  42831  pell1qr1  42841  pellqrexplicit  42847  rmxycomplete  42888  dgraalem  43116  tfsconcatrev  43319  clsk3nimkb  44011  fourierdlem64  46147  rspceaov  47174  ichnreuop  47434  prelspr  47448  reuopreuprim  47488  6gbe  47733  7gbow  47734  8gbe  47735  9gbo  47736  11gbo  47737  modn0mul  48448  elbigo2r  48481  rrx2xpref1o  48646  inlinecirc02plem  48714  sepfsepc  48850  iscnrm3lem7  48861