Theorem sbequ12 2097

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.)

Assertion

Ref	Expression
sbequ12	⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Proof of Theorem sbequ12

Step	Hyp	Ref	Expression
1		sbequ1 2096	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 1869	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 201	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 195  [wsb 1867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-sb 1868

This theorem is referenced by:  sbequ12r  2098  sbequ12a  2099  axc16ALT  2354  nfsb4t  2377  sbco2  2403  sb8  2412  sb8e  2413  sbal1  2448  clelab  2735  sbab  2737  cbvralf  3141  cbvralsv  3158  cbvrexsv  3159  cbvrab  3171  sbhypf  3226  mob2  3353  reu2  3361  reu6  3362  sbcralt  3477  sbcreu  3482  cbvreucsf  3533  cbvrabcsf  3534  csbif  4088  rabasiun  4459  cbvopab1  4655  cbvopab1s  4657  cbvmptf  4676  cbvmpt  4677  opelopabsb  4910  csbopab  4932  csbopabgALT  4933  opeliunxp  5093  ralxpf  5190  cbviota  5773  csbiota  5797  cbvriota  6521  csbriota  6523  onminex  6899  tfis  6946  findes  6988  abrexex2g  7036  opabex3d  7037  opabex3  7038  abrexex2  7040  dfoprab4f  7117  uzind4s  11624  ac6sf2  28810  esumcvg  29475  bj-sbab  31972  wl-sb8t  32512  wl-sbalnae  32524  wl-ax11-lem8  32548  sbcrexgOLD  36367  pm13.193  37634  opeliun2xp  41904