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

Theorem vtocl2ga 3159
Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 20-Aug-1995.)
Hypotheses
Ref Expression
vtocl2ga.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
vtocl2ga.2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
vtocl2ga.3  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ph )
Assertion
Ref Expression
vtocl2ga  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ch )
Distinct variable groups:    x, y, A    y, B    x, C, y    x, D, y    ps, x    ch, y
Allowed substitution hints:    ph( x, y)    ps( y)    ch( x)    B( x)

Proof of Theorem vtocl2ga
StepHypRef Expression
1 nfcv 2603 . 2  |-  F/_ x A
2 nfcv 2603 . 2  |-  F/_ y A
3 nfcv 2603 . 2  |-  F/_ y B
4 nfv 1692 . 2  |-  F/ x ps
5 nfv 1692 . 2  |-  F/ y ch
6 vtocl2ga.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
7 vtocl2ga.2 . 2  |-  ( y  =  B  ->  ( ps 
<->  ch ) )
8 vtocl2ga.3 . 2  |-  ( ( x  e.  C  /\  y  e.  D )  ->  ph )
91, 2, 3, 4, 5, 6, 7, 8vtocl2gaf 3158 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1381    e. wcel 1802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095
This theorem is referenced by:  solin  4809  caovcan  6460  pwfseqlem2  9035  mulcanenq  9336  ltaddnq  9350  ltrnq  9355  genpv  9375  wrdind  12676  fsumrelem  13595  imasleval  14810  fullfunc  15144  fthfunc  15145  pf1ind  18259  mretopd  19459  dvlip  22260  scvxcvx  23180  issubgoilem  25176  cnre2csqlem  27758
  Copyright terms: Public domain W3C validator