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

Syntax hints:   → wi 4   ↔ wb 209  [wsb 2070

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 1912  ax-6 1971  ax-7 2016  ax-12 2176

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071

This theorem is referenced by:  sbequ12r  2252  sbequ12a  2254  sb5  2274  sb8v  2363  sb8ev  2364  sbbib  2370  axc16ALT  2508  nfsb4t  2518  sbco2  2531  sb8  2537  sb8e  2538  sbal1  2549  sbal2  2550  clelabOLD  2897  sbab  2899  nfabdw  2941  cbvralfwOLD  3349  cbvralf  3351  cbvralsvw  3380  cbvrexsvw  3381  cbvralsv  3382  cbvrexsv  3383  cbvrabw  3403  cbvrab  3404  sbhypf  3470  mob2  3630  reu2  3640  reu6  3641  sbcralt  3779  sbcreu  3783  cbvrabcsfw  3847  cbvreucsf  3850  cbvrabcsf  3851  csbif  4478  cbvopab1  5106  cbvopab1g  5107  cbvopab1s  5109  cbvmptf  5132  cbvmptfg  5133  csbopab  5413  csbopabgALT  5414  opeliunxp  5589  ralxpf  5687  cbviotaw  6302  cbviota  6304  csbiota  6329  f1ossf1o  6882  cbvriotaw  7118  cbvriota  7122  csbriota  7124  onminex  7522  tfis  7569  findes  7613  abrexex2g  7670  opabex3d  7671  opabex3rd  7672  opabex3  7673  dfoprab4f  7759  uzind4s  12341  ac6sf2  30475  esumcvg  31566  wl-sb8t  35226  wl-sbalnae  35236  wl-ax11-lem8  35262  sbcrexgOLD  40092  scottabes  41316  pm13.193  41481  2reu8i  44030  ichnfimlem  44341  opeliun2xp  45094