Theorem sbceq1a 3750

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

Assertion

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

Proof of Theorem sbceq1a

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3740

This theorem is used by:  sbceq2a  3751  elrabsf  3784  cbvralcsf  3889  reusngf  4635  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5490  reuop  6291  frpoinsg  6341  elfvmptrab1w  7014  elfvmptrab1  7015  ralrnmpt  7089  riotass2  7400  riotass  7401  oprabv  7473  elovmporab  7660  elovmporab1w  7661  elovmporab1  7662  ovmpt3rabdm  7673  elovmpt3rab1  7674  tfisg  7850  tfindes  7859  sbcopeq1a  8046  sbcoteq1a  8048  mpoxopoveq  8217  findcard2  9159  ac6sfi  9254  indexfi  9327  setinds  9728  frinsg  9733  nn0ind-raph  12721  fzrevral  13667  wrdind  14791  wrd2ind  14792  prmind2  16775  elmptrab  24053  isfildlem  24083  2sqreulem4  27690  gropd  29488  grstructd  29489  rspc2daf  32942  opreu2reuALT  32952  ifeqeqx  33017  wrdt2ind  33395  bnj919  35277  bnj976  35287  bnj1468  35355  bnj110  35367  bnj150  35385  bnj151  35386  bnj607  35425  bnj873  35433  bnj849  35434  bnj1388  35542  dfon2lem1  36360  rdgssun  38132  indexdom  38484  sdclem2  38492  sdclem1  38493  fdc1  38496  riotasv2s  39831  elimhyps  39834  sbccomieg  43634  rexrabdioph  43635  rexfrabdioph  43636  aomclem6  43900  pm13.13a  45231  pm13.13b  45232  pm13.14  45233  tratrb  45359  uzwo4  45887  or2expropbilem2  47921  reuf1odnf  47995  ich2exprop  48371  ichnreuop  48372  ichreuopeq  48373  prproropreud  48409  reupr  48422  reuopreuprim  48426