Theorem sbequ12 2251

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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065

This theorem is referenced by:  sbequ12r  2252  sbequ12a  2254  sb8fOLD  2357  sb8ef  2358  sbbib  2364  axc16ALT  2494  nfsb4t  2504  sbco2  2516  sb8  2522  sb8e  2523  sbal1  2533  sbal2  2534  sbab  2889  cbvrexsvw  3318  cbvralsvwOLD  3319  cbvralsvwOLDOLD  3320  cbvrexsvwOLD  3321  cbvralf  3360  cbvralsv  3366  cbvrexsv  3367  cbvrabwOLD  3474  cbvrab  3479  sbhypfOLD  3545  mob2  3721  reu2  3731  reu6  3732  sbcralt  3872  sbcreu  3876  cbvrabcsfw  3940  cbvreucsf  3943  cbvrabcsf  3944  csbif  4583  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  cbvmptf  5251  cbvmptfg  5252  csbopab  5560  csbopabgALT  5561  opeliunxp  5752  opeliun2xp  5753  ralxpf  5857  cbviotaw  6521  cbviota  6523  csbiota  6554  f1ossf1o  7148  cbvriotaw  7397  cbvriota  7401  csbriota  7403  onminex  7822  tfis  7876  findes  7922  abrexex2g  7989  opabex3d  7990  opabex3rd  7991  opabex3  7992  dfoprab4f  8081  uzind4s  12950  ac6sf2  32634  esumcvg  34087  wl-sb8t  37553  wl-sbalnae  37563  wl-ax11-lem8  37593  sbcrexgOLD  42796  scottabes  44261  pm13.193  44430  2reu8i  47125  ichnfimlem  47450