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

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

Proof of Theorem rspc2va
StepHypRef Expression
1 rspc2v.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜒))
2 rspc2v.2 . . 3 (𝑦 = 𝐵 → (𝜒𝜓))
31, 2rspc2v 3453 . 2 ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
43imp 444 1 (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-v 3334
This theorem is referenced by:  swopo  5189  soisores  6732  soisoi  6733  isocnv  6735  isotr  6741  ovrspc2v  6827  off  7069  caofrss  7087  caonncan  7092  wunpr  9715  injresinj  12775  seqcaopr2  13023  rlimcn2  14512  o1of2  14534  isprm6  15620  ssc2  16675  pospropd  17327  mhmpropd  17534  grpidssd  17684  grpinvssd  17685  dfgrp3lem  17706  isnsg3  17821  symgextf1  18033  efgredlemd  18349  efgredlem  18352  issrngd  19055  domneq0  19491  mplsubglem  19628  lindfind  20349  lindsind  20350  mdetunilem1  20612  mdetunilem3  20614  mdetunilem4  20615  mdetunilem9  20620  decpmatmulsumfsupp  20772  pm2mpf1  20798  pm2mpmhmlem1  20817  t0sep  21322  tsmsxplem2  22150  comet  22511  nrmmetd  22572  tngngp  22651  reconnlem2  22823  iscmet3lem1  23281  iscmet3lem2  23282  dchrisumlem1  25369  pntpbnd1  25466  motcgr  25622  perpneq  25800  foot  25805  f1otrg  25942  axcontlem10  26044  frgr2wwlk1  27475  tleile  29962  orngmul  30104  mndpluscn  30273  unelros  30535  difelros  30536  inelsros  30542  diffiunisros  30543  cvxsconn  31524  elmrsubrn  31716  ghomco  33995  mzpcl34  37788  ntrk0kbimka  38831  isotone1  38840  isotone2  38841  nnfoctbdjlem  41167  mgmhmpropd  42287  rnghmmul  42402
  Copyright terms: Public domain W3C validator