Theorem sbceq1a 3479

Description: Equality theorem for class substitution. Class version of sbequ12 2149. (Contributed by NM, 26-Sep-2003.)

Assertion

Ref	Expression
sbceq1a	⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2152	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3471	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	syl5bbr 274	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  [wsb 1937  [wsbc 3468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-sbc 3469

This theorem is referenced by:  sbceq2a  3480  elrabsf  3507  cbvralcsf  3598  rabsnifsb  4289  euotd  5004  wfisg  5753  elfvmptrab1  6344  ralrnmpt  6408  riotass2  6678  riotass  6679  oprabv  6745  elovmpt2rab  6922  elovmpt2rab1  6923  ovmpt3rabdm  6934  elovmpt3rab1  6935  tfindes  7104  sbcopeq1a  7264  mpt2xopoveq  7390  findcard2  8241  ac6sfi  8245  indexfi  8315  nn0ind-raph  11515  fzrevral  12463  wrdind  13522  wrd2ind  13523  prmind2  15445  elmptrab  21678  isfildlem  21708  gropd  25968  grstructd  25969  vtocl2d  29442  ifeqeqx  29487  bnj919  30963  bnj976  30974  bnj1468  31042  bnj110  31054  bnj150  31072  bnj151  31073  bnj607  31112  bnj873  31120  bnj849  31121  bnj1388  31227  setinds  31807  dfon2lem1  31812  tfisg  31840  frpoinsg  31866  frinsg  31870  indexdom  33659  sdclem2  33668  sdclem1  33669  fdc1  33672  riotasv2s  34562  elimhyps  34565  sbccomieg  37674  rexrabdioph  37675  rexfrabdioph  37676  aomclem6  37946  pm13.13a  38925  pm13.13b  38926  pm13.14  38927  tratrb  39063  uzwo4  39535