Theorem vtoclg 1843

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 969	. 2 |- (y e. A -> A.x y e. A)
2		ax-17 969	. 2 |- (ps -> A.xps)
3		vtoclg.1	. 2 |- (x = A -> (ph <-> ps))
4		vtoclg.2	. 2 |- ph
5	1, 2, 3, 4	vtoclgf 1842	1 |- (A e. B -> ps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956

This theorem is referenced by:  vtoclbg 1844  ceqex 1882  moeq3 1917  mo2icl 1919  hbsbcg 1947  elpwg 2401  unisng 2513  elintg 2536  trel 2682  trss 2684  inex1g 2713  ssexg 2716  pwexg 2741  snex 2745  prex 2776  opprc1b 2791  opth2 2795  uniexg 2866  efrirr 2923  ordelord 2965  sucidg 3047  vtoclr 3206  vtoclrbr 3207  vtoclibr 3208  ididg 3273  breldmg 3311  resieq 3368  eliniseg 3421  funimaexg 3567  fneu 3584  fconstg 3650  tz6.12-2 3730  tz6.12i 3732  funopfvg 3743  fnbrfvb 3744  funbrfvbg 3748  fvelima 3755  ssimaexg 3760  fvelrn 3803  fvi 3833  abrexexg 3852  tfrlem10 3911  rdg0t 3935  op1stg 4077  ensn1g 4412  xpdom2 4428  canth2g 4471  pwen 4489  php2 4500  elirr 4579  unbnnt 4619  tz9.13g 4644  rankvalg 4649  rankr1g 4655  ranklim 4665  r1pw 4666  rankuni 4678  ac7g 4729  numth2 4765  numthcor 4766  fodomg 4779  sucxpdom 4826  prnmax 5079  ser1ft 6273  csbfsum 6973  climfnn 7038  infcvgaux2 7163  symggrp 10342  gelsupvalOLD 10354  filint2 10482

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain