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  2488  nfsb4t  2498  sbco2  2510  sb8  2516  sb8e  2517  sbal1  2527  sbal2  2528  clelabOLD  2880  sbab  2882  nfabdwOLD  2927  cbvralsvw  3314  cbvrexsvw  3315  cbvralsvwOLD  3316  cbvrexsvwOLD  3317  cbvralfwOLD  3320  cbvralf  3356  cbvralsv  3362  cbvrexsv  3363  cbvrabw  3467  cbvrab  3473  sbhypfOLD  3539  mob2  3711  reu2  3721  reu6  3722  sbcralt  3866  sbcreu  3870  cbvrabcsfw  3937  cbvreucsf  3940  cbvrabcsf  3941  csbif  4585  cbvopab1  5223  cbvopab1g  5224  cbvopab1s  5226  cbvmptf  5257  cbvmptfg  5258  csbopab  5555  csbopabgALT  5556  opeliunxp  5743  ralxpf  5846  cbviotaw  6502  cbviota  6505  csbiota  6536  f1ossf1o  7128  cbvriotaw  7376  cbvriota  7381  csbriota  7383  onminex  7792  tfis  7846  findes  7895  abrexex2g  7953  opabex3d  7954  opabex3rd  7955  opabex3  7956  dfoprab4f  8044  uzind4s  12896  ac6sf2  32104  esumcvg  33370  wl-sb8t  36720  wl-sbalnae  36730  wl-ax11-lem8  36757  sbcrexgOLD  41825  scottabes  43303  pm13.193  43472  2reu8i  46120  ichnfimlem  46430  opeliun2xp  47097