Theorem sbceq1a 1941

Description: Equality theorem for class substitution.

Assertion

Ref	Expression
sbceq1a	⊢ (x = A → (φ ↔ [A / x]φ))

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		dfsbcq 1940	. 2 ⊢ (x = A → ([x / x]φ ↔ [A / x]φ))
2		sbid 1183	. 2 ⊢ ([x / x]φ ↔ φ)
3	1, 2	syl5bbr 533	1 ⊢ (x = A → (φ ↔ [A / x]φ))

Syntax hints:   → wi 3   ↔ wb 146   = wceq 955  [wsbc 1169

This theorem is referenced by:  sbc5g 1951  sbc6g 1952  elrabsf 1960  sbcel1gv 1977  sbcel2gv 1978  sbcbrg 2658  reuuni4 2883  reuuniss 2885  reuuniss2 2887  sbcopeq1a 4104  dfopab2 4106  dfoprab3 4107  nn1suc 5897  uzindOLD 6166  nn0ind-raph 6172  fzrevralt 6464

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-cleq 1468  df-clel 1471  df-sbc 1939

Copyright terms: Public domain