Theorem sbceq1a 3756

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2096  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746

This theorem is referenced by:  sbceq2a  3757  elrabsf  3790  cbvralcsf  3896  reusngf  4641  rexreusng  4646  reuprg0  4669  rmosn  4686  rabsnifsb  4689  euotd  5498  reuop  6296  frpoinsg  6346  elfvmptrab1w  7019  elfvmptrab1  7020  ralrnmpt  7093  riotass2  7399  riotass  7400  oprabv  7472  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  ovmpt3rabdm  7671  elovmpt3rab1  7672  tfisg  7851  tfindes  7860  sbcopeq1a  8047  sbcoteq1a  8049  mpoxopoveq  8216  findcard2  9150  ac6sfi  9245  indexfi  9318  setinds  9719  frinsg  9724  nn0ind-raph  12697  fzrevral  13642  wrdind  14761  wrd2ind  14762  prmind2  16744  elmptrab  23965  isfildlem  23995  2sqreulem4  27599  gropd  29362  grstructd  29363  rspc2daf  32794  opreu2reuALT  32804  ifeqeqx  32869  wrdt2ind  33254  bnj919  35137  bnj976  35147  bnj1468  35215  bnj110  35227  bnj150  35245  bnj151  35246  bnj607  35285  bnj873  35293  bnj849  35294  bnj1388  35402  dfon2lem1  36254  rdgssun  38005  indexdom  38366  sdclem2  38374  sdclem1  38375  fdc1  38378  riotasv2s  39713  elimhyps  39716  sbccomieg  43503  rexrabdioph  43504  rexfrabdioph  43505  aomclem6  43769  pm13.13a  45100  pm13.13b  45101  pm13.14  45102  tratrb  45228  uzwo4  45756  or2expropbilem2  47753  reuf1odnf  47827  ich2exprop  48203  ichnreuop  48204  ichreuopeq  48205  prproropreud  48241  reupr  48254  reuopreuprim  48258