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

Theorem rspc2va 3571
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 3570 . 2 ((𝐴𝐶𝐵𝐷) → (∀𝑥𝐶𝑦𝐷 𝜑𝜓))
43imp 407 1 (((𝐴𝐶𝐵𝐷) ∧ ∀𝑥𝐶𝑦𝐷 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wral 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069
This theorem is referenced by:  swopo  5514  soisores  7198  soisoi  7199  isocnv  7201  isotr  7207  ovrspc2v  7301  caofrss  7569  caonncan  7574  wunpr  10465  injresinj  13508  seqcaopr2  13759  rlimcn3  15299  o1of2  15322  isprm6  16419  ssc2  17534  pospropd  18045  tleile  18139  mhmpropd  18436  grpidssd  18651  grpinvssd  18652  dfgrp3lem  18673  isnsg3  18788  cyccom  18822  symgextf1  19029  efgredlemd  19350  efgredlem  19353  issrngd  20121  domneq0  20568  lindfind  21023  lindsind  21024  mplsubglem  21205  mdetunilem1  21761  mdetunilem3  21763  mdetunilem4  21764  mdetunilem9  21769  decpmatmulsumfsupp  21922  pm2mpf1  21948  pm2mpmhmlem1  21967  t0sep  22475  tsmsxplem2  23305  comet  23669  nrmmetd  23730  tngngp  23818  reconnlem2  23990  iscmet3lem1  24455  iscmet3lem2  24456  dchrisumlem1  26637  pntpbnd1  26734  tgjustc1  26836  tgjustc2  26837  iscgrglt  26875  motcgr  26897  perpneq  27075  foot  27083  f1otrg  27232  axcontlem10  27341  frgr2wwlk1  28693  orngmul  31502  lindsunlem  31705  mndpluscn  31876  unelros  32139  difelros  32140  inelsros  32146  diffiunisros  32147  cvxsconn  33205  elmrsubrn  33482  frpoins3xpg  33787  ssltsepc  33987  ghomco  36049  sticksstones10  40111  sticksstones12a  40113  fsuppind  40279  mzpcl34  40553  ntrk0kbimka  41649  isotone1  41658  isotone2  41659  nnfoctbdjlem  43993  isomuspgrlem2d  45283  mgmhmpropd  45339  rnghmmul  45458  2arymaptf1  45999
  Copyright terms: Public domain W3C validator