Theorem rspc2ev 3581

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ∃wrex 3070

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071

This theorem is referenced by:  rspc3ev  3583  opelxp  5650  fprb  7119  f1prex  7206  nf1const  7226  rspceov  7376  erov  8666  ralxpmap  8747  2dom  8887  elfiun  9279  dffi3  9280  ixpiunwdom  9439  1re  11068  hashdmpropge2  14289  wrdl2exs2  14750  ello12r  15317  ello1d  15323  elo12r  15328  o1lo1  15337  addcn2  15394  mulcn2  15396  bezoutlem3  16340  bezout  16342  pythagtriplem18  16622  pczpre  16637  pcdiv  16642  4sqlem3  16740  4sqlem4  16742  4sqlem12  16746  vdwlem1  16771  vdwlem6  16776  vdwlem8  16778  vdwlem12  16782  vdwlem13  16783  0ram  16810  ramz2  16814  cat1lem  17900  sgrp2rid2ex  18654  pmtr3ncom  19171  psgnunilem1  19189  irredn0  20032  isnzr2  20632  hausnei2  22602  cnhaus  22603  dishaus  22631  ordthauslem  22632  txuni2  22814  xkoopn  22838  txopn  22851  txdis  22881  txdis1cn  22884  pthaus  22887  txhaus  22896  tx1stc  22899  xkohaus  22902  regr1lem  22988  qustgplem  23370  methaus  23774  met2ndci  23776  metnrmlem3  24122  elplyr  25460  aaliou2b  25599  aaliou3lem9  25608  2irrexpq  25983  2irrexpqALT  26048  2sqlem2  26664  2sqlem8  26672  2sqlem11  26675  2sqb  26678  2sqnn0  26684  2sqnn  26685  pntibnd  26839  legov  27176  iscgrad  27402  f1otrge  27463  axsegconlem1  27515  axsegcon  27525  axpaschlem  27538  axlowdimlem6  27545  axlowdim1  27557  axlowdim2  27558  axeuclidlem  27560  umgrvad2edg  27810  wwlksnwwlksnon  28509  upgr4cycl4dv4e  28778  3cyclfrgrrn1  28878  4cycl2vnunb  28883  br8d  31178  lt2addrd  31302  xlt2addrd  31309  xrnarchi  31666  txomap  32023  tpr2rico  32101  qqhval2  32171  elsx  32401  br2base  32477  dya2iocnrect  32489  connpconn  33437  satfv1fvfmla1  33625  br8  33956  br4  33958  madecut  34156  brsegle  34501  hilbert1.1  34547  nn0prpwlem  34602  knoppndvlem21  34803  poimirlem1  35876  itg2addnclem3  35928  cntotbnd  36052  smprngopr  36308  3dim2  37729  llni2  37773  lvoli3  37838  lvoli2  37842  islinei  38001  psubspi2N  38009  elpaddri  38063  2rspcedvdw  40430  eldioph2lem1  40832  diophin  40844  fphpdo  40889  irrapxlem3  40896  irrapxlem4  40897  pellexlem6  40906  pell1234qrreccl  40926  pell1234qrmulcl  40927  pell1234qrdich  40933  pell1qr1  40943  pellqrexplicit  40949  rmxycomplete  40990  dgraalem  41221  clsk3nimkb  41960  fourierdlem64  44036  rspceaov  45029  ichnreuop  45264  prelspr  45278  reuopreuprim  45318  6gbe  45563  7gbow  45564  8gbe  45565  9gbo  45566  11gbo  45567  modn0mul  46206  elbigo2r  46239  rrx2xpref1o  46404  inlinecirc02plem  46472  sepfsepc  46561  iscnrm3lem7  46573