Theorem sbceq1d 3744

Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)

Hypothesis

Ref	Expression
sbceq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sbceq1d	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

Proof of Theorem sbceq1d

Step	Hyp	Ref	Expression
1		sbceq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfsbcq 3741	. 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))
3	1, 2	syl 18	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [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-ext 2732

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

This theorem is used by:  sbceq1dd  3745  sbcnestgfw  4379  sbcnestgf  4384  ralrnmptw  7087  ralrnmpt  7089  tfindes  7859  findes  7897  frpoins3xpg  8138  frpoins3xp3g  8139  findcard2  9159  ac6sfi  9254  indexfi  9327  ac6num  10481  nn1suc  12279  uzind4s  12957  uzind4s2  12958  fzrevral  13667  fzshftral  13670  fi1uzind  14572  wrdind  14791  wrd2ind  14792  cjth  15190  prmind2  16775  isprs  18384  isdrs  18389  joinlem  18469  meetlem  18483  istos  18504  isdlat  18610  gsumvalx  18778  mndind  18937  issrg  20327  islmod  21048  quotval  26522  nn0min  33291  wrdt2ind  33395  bnj944  35447  sdclem2  38492  fdc  38495  hdmap1ffval  42668  hdmap1fval  42669  rexrabdioph  43635  2nn0ind  43786  zindbi  43787  iotasbcq  45260  prproropreud  48409