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

Theorem vtocl2ga 3100
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 2544 . 2  |-  F/_ x A
2 nfcv 2544 . 2  |-  F/_ y A
3 nfcv 2544 . 2  |-  F/_ y B
4 nfv 1715 . 2  |-  F/ x ps
5 nfv 1715 . 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 3099 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036
This theorem is referenced by:  solin  4737  caovcan  6378  pwfseqlem2  8948  mulcanenq  9249  ltaddnq  9263  ltrnq  9268  genpv  9288  wrdind  12613  fsumrelem  13623  imasleval  14948  fullfunc  15312  fthfunc  15313  pf1ind  18504  mretopd  19679  dvlip  22479  scvxcvx  23432  issubgoilem  25428  cnre2csqlem  28046
  Copyright terms: Public domain W3C validator