Theorem sbceq1a 1915

Description: Equality theorem for class substitution.

Assertion

Ref	Expression
sbceq1a	|- (x = A -> (ph <-> [A / x]ph))

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		dfsbcq 1914	. 2 |- (x = A -> ([x / x]ph <-> [A / x]ph))
2		sbid 1167	. 2 |- ([x / x]ph <-> ph)
3	1, 2	syl5bbr 532	1 |- (x = A -> (ph <-> [A / x]ph))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 1099  [wsbc 1153

This theorem is referenced by:  sbc5g 1925  sbc6g 1926  elrabsf 1934  sbcel1gv 1951  sbcel2gv 1952  sbcbrg 2630  reuuni4 2850  reuuniss 2852  reuuniss2 2854  sbcopeq1a 4049  dfopab2 4051  dfoprab3 4052  nn1suc 5838  uzindOLD 6107  nn0ind-raph 6113  fzrevralt 6402

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104  ax-17 1190  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-cleq 1446  df-clel 1449  df-sbc 1913

Copyright terms: Public domain