HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem gencl 1819
Description: Implicit substitution for class with embedded variable.
Hypotheses
Ref Expression
gencl.1 |- (th <-> E.x(ch /\ A = B))
gencl.2 |- (A = B -> (ph <-> ps))
gencl.3 |- (ch -> ph)
Assertion
Ref Expression
gencl |- (th -> ps)
Distinct variable group:   ps,x
Proof of Theorem gencl
StepHypRef Expression
1 gencl.1 . 2 |- (th <-> E.x(ch /\ A = B))
2 gencl.2 . . . . 5 |- (A = B -> (ph <-> ps))
3 gencl.3 . . . . 5 |- (ch -> ph)
42, 3syl5bi 208 . . . 4 |- (A = B -> (ch -> ps))
54impcom 351 . . 3 |- ((ch /\ A = B) -> ps)
6519.23aiv 1290 . 2 |- (E.x(ch /\ A = B) -> ps)
71, 6sylbi 199 1 |- (th -> ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953  E.wex 977
This theorem is referenced by:  2gencl 1820  3gencl 1821  indpi 5006  axrnegex 5255  axrrecex 5256
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978
Copyright terms: Public domain