Theorem sbceq1a 3761

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

Assertion

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

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2256	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3753	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 285	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065  [wsbc 3750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3751

This theorem is referenced by:  sbceq2a  3762  elrabsf  3796  cbvralcsf  3901  reusngf  4634  rexreusng  4639  reuprg0  4662  rmosn  4679  rabsnifsb  4682  euotd  5468  reuop  6254  frpoinsg  6304  elfvmptrab1w  6977  elfvmptrab1  6978  ralrnmpt  7050  riotass2  7356  riotass  7357  oprabv  7429  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  ovmpt3rabdm  7628  elovmpt3rab1  7629  tfisg  7810  tfindes  7819  sbcopeq1a  8007  sbcoteq1a  8009  mpoxopoveq  8175  findcard2  9105  ac6sfi  9207  indexfi  9287  frinsg  9680  nn0ind-raph  12610  fzrevral  13549  wrdind  14663  wrd2ind  14664  prmind2  16631  elmptrab  23690  isfildlem  23720  2sqreulem4  27341  gropd  28934  grstructd  28935  rspc2daf  32368  opreu2reuALT  32379  ifeqeqx  32444  wrdt2ind  32848  bnj919  34730  bnj976  34740  bnj1468  34809  bnj110  34821  bnj150  34839  bnj151  34840  bnj607  34879  bnj873  34887  bnj849  34888  bnj1388  34996  setinds  35739  dfon2lem1  35744  rdgssun  37339  indexdom  37701  sdclem2  37709  sdclem1  37710  fdc1  37713  riotasv2s  38924  elimhyps  38927  sbccomieg  42754  rexrabdioph  42755  rexfrabdioph  42756  aomclem6  43021  pm13.13a  44369  pm13.13b  44370  pm13.14  44371  tratrb  44499  uzwo4  45020  or2expropbilem2  47007  reuf1odnf  47081  ich2exprop  47445  ichnreuop  47446  ichreuopeq  47447  prproropreud  47483  reupr  47496  reuopreuprim  47500