Theorem sbequ12 2244

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2172

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069

This theorem is referenced by:  sbequ12r  2245  sbequ12a  2247  sb5OLD  2269  sb8fOLD  2351  sb8ef  2352  sbbib  2358  axc16ALT  2489  nfsb4t  2499  sbco2  2511  sb8  2517  sb8e  2518  sbal1  2528  sbal2  2529  clelabOLD  2881  sbab  2883  nfabdwOLD  2928  cbvralsvw  3315  cbvrexsvw  3316  cbvralsvwOLD  3317  cbvrexsvwOLD  3318  cbvralfwOLD  3321  cbvralf  3357  cbvralsv  3363  cbvrexsv  3364  cbvrabw  3468  cbvrab  3474  sbhypfOLD  3539  mob2  3710  reu2  3720  reu6  3721  sbcralt  3865  sbcreu  3869  cbvrabcsfw  3936  cbvreucsf  3939  cbvrabcsf  3940  csbif  4584  cbvopab1  5222  cbvopab1g  5223  cbvopab1s  5225  cbvmptf  5256  cbvmptfg  5257  csbopab  5554  csbopabgALT  5555  opeliunxp  5741  ralxpf  5844  cbviotaw  6499  cbviota  6502  csbiota  6533  f1ossf1o  7121  cbvriotaw  7369  cbvriota  7374  csbriota  7376  onminex  7785  tfis  7839  findes  7888  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfoprab4f  8037  uzind4s  12888  ac6sf2  31827  esumcvg  33022  wl-sb8t  36355  wl-sbalnae  36365  wl-ax11-lem8  36392  sbcrexgOLD  41456  scottabes  42934  pm13.193  43103  2reu8i  45756  ichnfimlem  46066  opeliun2xp  46910