Theorem vtoclbg 1839

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 627	. 2 |- (x = A -> ((ph <-> ps) <-> (ch <-> th)))
4		vtoclbg.3	. 2 |- (ph <-> ps)
5	3, 4	vtoclg 1838	1 |- (A e. B -> (ch <-> th))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955

This theorem is referenced by:  eqvinc 1874  sbccog 1942  sbcng 1959  sbcimg 1960  sbcang 1961  sbcorg 1962  sbcbidig 1963  sbcalg 1964  sbcexg 1965  snssg 2454  elintrabg 2536  opthg 2778  elopab 2800  elomg 3125  opelxp 3204  opelxpg 3206  eldm2g 3298  opelresg 3358  ndmfv 3730  funfvima3 3839  domeng 4362

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain