Theorem sbequ12 2243

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 2240	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2241	. 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑))
3	1, 2	impbid 211	1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068

This theorem is referenced by:  sbequ12r  2244  sbequ12a  2246  sb5OLD  2268  sb8fOLD  2350  sb8ef  2351  sbbib  2357  axc16ALT  2487  nfsb4t  2497  sbco2  2509  sb8  2515  sb8e  2516  sbal1  2526  sbal2  2527  clelabOLD  2879  sbab  2881  nfabdwOLD  2926  cbvralsvw  3298  cbvrexsvw  3299  cbvralfwOLD  3302  cbvralf  3331  cbvralsv  3337  cbvrexsv  3338  cbvrabw  3440  cbvrab  3445  sbhypfOLD  3509  mob2  3676  reu2  3686  reu6  3687  sbcralt  3831  sbcreu  3835  cbvrabcsfw  3902  cbvreucsf  3905  cbvrabcsf  3906  csbif  4548  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvmptf  5219  cbvmptfg  5220  csbopab  5517  csbopabgALT  5518  opeliunxp  5704  ralxpf  5807  cbviotaw  6460  cbviota  6463  csbiota  6494  f1ossf1o  7079  cbvriotaw  7327  cbvriota  7332  csbriota  7334  onminex  7742  tfis  7796  findes  7844  abrexex2g  7902  opabex3d  7903  opabex3rd  7904  opabex3  7905  dfoprab4f  7993  uzind4s  12842  ac6sf2  31606  esumcvg  32774  wl-sb8t  36080  wl-sbalnae  36090  wl-ax11-lem8  36117  sbcrexgOLD  41166  scottabes  42644  pm13.193  42813  2reu8i  45465  ichnfimlem  45775  opeliun2xp  46528