MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc2ev Unicode version

Theorem rspc2ev 3221
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:   , ,   ,   ,   , ,   ,   ,

Proof of Theorem rspc2ev
StepHypRef Expression
1 rspc2v.2 . . . . 5
21rspcev 3210 . . . 4
32anim2i 569 . . 3
433impb 1192 . 2
5 rspc2v.1 . . . 4
65rexbidv 2968 . . 3
76rspcev 3210 . 2
84, 7syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  E.wrex 2808
This theorem is referenced by:  rspc3ev  3223  opelxp  5034  rspceov  6336  erov  7427  ralxpmap  7488  2dom  7608  elfiun  7910  dffi3  7911  ixpiunwdom  8038  1re  9616  ello12r  13340  ello1d  13346  elo12r  13351  o1lo1  13360  addcn2  13416  mulcn2  13418  bezoutlem3  14178  bezout  14180  pythagtriplem18  14356  pczpre  14371  pcdiv  14376  4sqlem3  14468  4sqlem4  14470  4sqlem12  14474  vdwlem1  14499  vdwlem6  14504  vdwlem8  14506  vdwlem12  14510  vdwlem13  14511  0ram  14538  ramz2  14542  sgrp2rid2ex  16045  pmtr3ncom  16500  psgnunilem1  16518  irredn0  17352  isnzr2  17911  hausnei2  19854  cnhaus  19855  dishaus  19883  ordthauslem  19884  txuni2  20066  xkoopn  20090  txopn  20103  txdis  20133  txdis1cn  20136  pthaus  20139  txhaus  20148  tx1stc  20151  xkohaus  20154  regr1lem  20240  qustgplem  20619  methaus  21023  met2ndci  21025  metnrmlem3  21365  elplyr  22598  aaliou2b  22737  aaliou3lem9  22746  2sqlem2  23639  2sqlem8  23647  2sqlem11  23650  2sqb  23653  pntibnd  23778  legov  23972  f1otrge  24175  axsegconlem1  24220  axsegcon  24230  axpaschlem  24243  axlowdimlem6  24250  axlowdim1  24262  axlowdim2  24263  axeuclidlem  24265  el2wlksotot  24882  3cyclfrgrarn1  25012  4cycl2vnunb  25017  br8d  27463  lt2addrd  27563  xlt2addrd  27578  xrnarchi  27728  txomap  27837  tpr2rico  27894  qqhval2  27963  elsx  28165  isanmbfm  28227  br2base  28240  dya2iocnrect  28252  conpcon  28680  br8  29185  br4  29187  fprb  29203  brsegle  29758  hilbert1.1  29804  itg2addnclem3  30068  nn0prpwlem  30140  cntotbnd  30292  smprngopr  30449  eldioph2lem1  30693  diophin  30706  fphpdo  30751  irrapxlem3  30760  irrapxlem4  30761  pellexlem6  30770  pell1234qrreccl  30790  pell1234qrmulcl  30791  pell1234qrdich  30797  pell1qr1  30807  pellqrexplicit  30813  rmxycomplete  30853  dgraalem  31094  fourierdlem64  31953  rspceaov  32282  usgvad2edg  32411  3dim2  35192  llni2  35236  lvoli3  35301  lvoli2  35305  islinei  35464  psubspi2N  35472  elpaddri  35526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111
  Copyright terms: Public domain W3C validator