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

Theorem vtocl2ga 3144
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 2616 . 2  |-  F/_ x A
2 nfcv 2616 . 2  |-  F/_ y A
3 nfcv 2616 . 2  |-  F/_ y B
4 nfv 1674 . 2  |-  F/ x ps
5 nfv 1674 . 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 3143 1  |-  ( ( A  e.  C  /\  B  e.  D )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080
This theorem is referenced by:  solin  4773  caovcan  6378  pwfseqlem2  8938  mulcanenq  9241  ltaddnq  9255  ltrnq  9260  genpv  9280  wrdind  12490  fsumrelem  13389  imasleval  14599  fullfunc  14936  fthfunc  14937  pf1ind  17915  mretopd  18829  dvlip  21599  scvxcvx  22513  issubgoilem  23949  cnre2csqlem  26486
  Copyright terms: Public domain W3C validator