MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rspc2v Structured version   Visualization version   GIF version

Theorem rspc2v 3584
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.)
Hypotheses
Ref Expression
rspc2v.1 (𝑥 = 𝐴 → (𝜑𝜒))
rspc2v.2 (𝑦 = 𝐵 → (𝜒𝜓))
Assertion
Ref Expression
rspc2v ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶   𝑥,𝐷,𝑦   𝜒,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥)   𝜒(𝑦)   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem rspc2v
StepHypRef Expression
1 rspc2v.1 . . . 4 (𝑥 = 𝐴 → (𝜑𝜒))
21ralbidv 3165 . . 3 (𝑥 = 𝐴 → (∀𝑦𝐷 𝜑 ↔ ∀𝑦𝐷 𝜒))
32rspcv 3569 . 2 (𝐴𝐶 → (∀𝑥𝐶𝑦𝐷 𝜑 → ∀𝑦𝐷 𝜒))
4 rspc2v.2 . . 3 (𝑦 = 𝐵 → (𝜒𝜓))
54rspcv 3569 . 2 (𝐵𝐷 → (∀𝑦𝐷 𝜒𝜓))
63, 5sylan9 511 1 ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  wral 3109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873  df-ral 3114
This theorem is referenced by:  rspc2va  3585  rspc3v  3587  disji2  5015  f1veqaeq  6997  isorel  7062  isosolem  7083  oveqrspc2v  7166  fovcl  7262  caovclg  7324  caovcomg  7327  smoel  7984  fiint  8783  dffi3  8883  ltordlem  11158  seqhomo  13417  cshf1  14167  climcn2  14944  drsdir  17540  tsrlin  17824  dirge  17842  mhmlin  17958  issubg2  18289  nsgbi  18304  ghmlin  18358  efgi  18840  efgred  18869  irredmul  19458  issubrg2  19551  abvmul  19596  abvtri  19597  lmodlema  19635  islmodd  19636  rmodislmodlem  19697  rmodislmod  19698  lmhmlin  19803  lbsind  19848  ipcj  20326  obsip  20413  mplcoe5lem  20710  matecl  21033  dmatelnd  21104  scmateALT  21120  mdetdiaglem  21206  mdetdiagid  21208  pmatcoe1fsupp  21309  m2cpminvid2lem  21362  inopn  21507  basis1  21558  basis2  21559  iscldtop  21703  hausnei  21936  t1sep2  21977  nconnsubb  22031  r0sep  22356  fbasssin  22444  fcfneii  22645  ustssel  22814  xmeteq0  22948  tngngp3  23265  nmvs  23285  cncfi  23502  c1lip1  24603  aalioulem3  24933  logltb  25194  cvxcl  25573  2sqlem8  26013  axtgcgrrflx  26259  axtgsegcon  26261  axtg5seg  26262  axtgbtwnid  26263  axtgpasch  26264  axtgcont1  26265  axtgupdim2  26268  axtgeucl  26269  isperp2d  26513  f1otrgds  26666  brbtwn2  26702  axcontlem3  26763  axcontlem9  26769  axcontlem10  26770  upgrwlkdvdelem  27528  conngrv2edg  27983  frgrwopreglem5ALT  28110  ablocom  28334  nvs  28449  nvtri  28456  phpar2  28609  phpar  28610  shaddcl  29003  shmulcl  29004  cnopc  29699  unop  29701  hmop  29708  cnfnc  29716  adj1  29719  hstel2  30005  stj  30021  stcltr1i  30060  mddmdin0i  30217  cdj3lem1  30220  cdj3lem2b  30223  disji2f  30343  disjif2  30347  disjxpin  30354  fovcld  30402  isoun  30464  archirng  30870  archiexdiv  30872  slmdlema  30884  inelcarsg  31677  sibfof  31706  breprexplema  32009  axtgupdim2ALTV  32047  pconncn  32579  nocvxminlem  33355  ivthALT  33791  poimirlem32  35082  ismtycnv  35233  ismtyima  35234  ismtyres  35239  bfplem1  35253  bfplem2  35254  ghomlinOLD  35319  rngohomadd  35400  rngohommul  35401  crngocom  35432  idladdcl  35450  idllmulcl  35451  idlrmulcl  35452  pridl  35468  ispridlc  35501  pridlc  35502  dmnnzd  35506  oposlem  36471  omllaw  36532  hlsuprexch  36670  lautle  37373  ltrnu  37410  tendovalco  38054  ntrkbimka  40728  mullimc  42245  mullimcf  42252  lptre2pt  42269  fourierdlem54  42789  faovcl  43743  icceuelpartlem  43939  iccpartnel  43942  fargshiftf1  43945  sprsymrelfolem2  43997  reuopreuprim  44030  mgmhmlin  44393  issubmgm2  44397
  Copyright terms: Public domain W3C validator