Theorem vtoclg 1893

Description: Implicit substitution of a class for a set variable.

Hypotheses

Ref	Expression
vtoclg.1	|- (x = A -> (ph <-> ps))
vtoclg.2	|- ph

Assertion

Ref	Expression
vtoclg	|- (A e. B -> ps)

Distinct variable groups:   x,A   ps,x

Proof of Theorem vtoclg

Step	Hyp	Ref	Expression
1		ax-17 1007	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 1007	. 2 |- (ps -> A.xps)
3		vtoclg.1	. 2 |- (x = A -> (ph <-> ps))
4		vtoclg.2	. 2 |- ph
5	1, 2, 3, 4	vtoclgf 1892	1 |- (A e. B -> ps)

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994

This theorem is referenced by:  vtoclbg 1894  ceqex 1932  moeq3 1967  mo2icl 1969  hbsbcg 1996  elpwg 2462  unisng 2585  elintg 2608  trel 2761  trss 2763  inex1g 2792  ssexg 2795  pwexg 2824  snex 2826  prex 2857  opprc1b 2872  opth2 2876  efrirr 2957  ordelord 2997  sucidg 3052  uniexg 3094  vtoclr 3294  vtoclrbr 3295  vtoclibr 3296  ididg 3368  breldmg 3407  resieq 3463  eliniseg 3521  funimaexg 3681  fneu 3698  fconstg 3766  tz6.12-2 3850  tz6.12i 3852  funopfvg 3863  fnbrfvb 3864  funbrfvbg 3868  fvelima 3875  ssimaexg 3880  fvelrn 3926  fvi 3956  abrexexg 3975  op1stg 4148  onfununi 4209  tfrlem10 4221  rdg0g 4245  ensn1g 4566  xpdom2 4583  canth2g 4630  pwen 4650  php2 4661  elirr 4742  unbnn3 4785  tz9.13g 4810  rankvalg 4815  rankr1g 4821  ranklim 4831  r1pw 4832  rankuni 4844  ac7g 4895  numth2 4931  numthcor 4932  fodomg 4945  sucxpdom 4996  prnmax 5253  ser1f 6693  csbfsum 7230  climfnn 7295  infcvgaux2i 7424  gx1 8318  gxnn0suc 8320  symggrp 10693  isppm 10917  on1el3 10962  filint2 11084  cbvcsb 11397  cbvsbc 11398  fictb 11423  ordtype 11434  fibas 11452  topfneec 11562  locfindsc 11576  ufilen 11664  dif1en 11833  acdcg 11842  acdc3g 11843  acdc5g 11844  incld 11899  mettrifi2 11913  bfplem8 12061

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858

Copyright terms: Public domain