HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem ceqex 1877
Description: Equality implies equivalence with substitution.
Assertion
Ref Expression
ceqex |- (x = A -> (ph <-> E.x(x = A /\ ph)))
Distinct variable group:   x,A
Proof of Theorem ceqex
StepHypRef Expression
1 19.8a 1025 . . 3 |- (x = A -> E.x x = A)
2 isset 1805 . . 3 |- (A e. V <-> E.x x = A)
31, 2sylibr 200 . 2 |- (x = A -> A e. V)
4 eqeq2 1476 . . . 4 |- (y = A -> (x = y <-> x = A))
54anbi1d 615 . . . . . 6 |- (y = A -> ((x = y /\ ph) <-> (x = A /\ ph)))
65exbidv 1274 . . . . 5 |- (y = A -> (E.x(x = y /\ ph) <-> E.x(x = A /\ ph)))
76bibi2d 616 . . . 4 |- (y = A -> ((ph <-> E.x(x = y /\ ph)) <-> (ph <-> E.x(x = A /\ ph))))
84, 7imbi12d 624 . . 3 |- (y = A -> ((x = y -> (ph <-> E.x(x = y /\ ph))) <-> (x = A -> (ph <-> E.x(x = A /\ ph)))))
9 19.8a 1025 . . . . 5 |- ((x = y /\ ph) -> E.x(x = y /\ ph))
109ex 373 . . . 4 |- (x = y -> (ph -> E.x(x = y /\ ph)))
11 ax-4 970 . . . . . 6 |- (A.x(x = y -> ph) -> (x = y -> ph))
1211com12 11 . . . . 5 |- (x = y -> (A.x(x = y -> ph) -> ph))
13 visset 1804 . . . . . 6 |- y e. V
1413alexeq 1876 . . . . 5 |- (A.x(x = y -> ph) <-> E.x(x = y /\ ph))
1512, 14syl5ibr 207 . . . 4 |- (x = y -> (E.x(x = y /\ ph) -> ph))
1610, 15impbid 514 . . 3 |- (x = y -> (ph <-> E.x(x = y /\ ph)))
178, 16vtoclg 1838 . 2 |- (A e. V -> (x = A -> (ph <-> E.x(x = A /\ ph))))
183, 17mpcom 49 1 |- (x = A -> (ph <-> E.x(x = A /\ ph)))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802
This theorem is referenced by:  ceqsexg 1878  copsexg 2782
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-16 1206  ax-11o 1213  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