Theorem vtoclbg 1848

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

Hypotheses

Ref	Expression
vtoclbg.1	|- (x = A -> (ph <-> ch))
vtoclbg.2	|- (x = A -> (ps <-> th))
vtoclbg.3	|- (ph <-> ps)

Assertion

Ref	Expression
vtoclbg	|- (A e. B -> (ch <-> th))

Distinct variable groups:   x,A   ch,x   th,x

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 |- (x = A -> (ph <-> ch))
2		vtoclbg.2	. . 3 |- (x = A -> (ps <-> th))
3	1, 2	bibi12d 629	. 2 |- (x = A -> ((ph <-> ps) <-> (ch <-> th)))
4		vtoclbg.3	. 2 |- (ph <-> ps)
5	3, 4	vtoclg 1847	1 |- (A e. B -> (ch <-> th))

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

This theorem is referenced by:  eqvinc 1883  sbccog 1952  sbcng 1969  sbcimg 1970  sbcang 1971  sbcorg 1972  sbcbidig 1973  sbcalg 1974  sbcexg 1975  snssg 2463  elintrabg 2546  opthg 2788  elopab 2811  elomg 3135  opelxp 3214  opelxpg 3216  eldm2g 3309  opelresg 3374  ndmfv 3745  funfvima3 3854  domeng 4380

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain