Theorem sbequ12 2253

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

Syntax hints:   → wi 4   ↔ wb 208  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070

This theorem is referenced by:  sbequ12r  2254  sbequ12a  2256  sb5  2276  sb8v  2373  sb8ev  2374  sbbib  2380  axc16ALT  2528  nfsb4t  2539  sbco2  2553  sb8  2559  sb8e  2560  sbal1  2572  sbal2  2573  clelab  2958  sbab  2960  nfabdw  3000  cbvralfw  3437  cbvralf  3439  cbvralsvw  3467  cbvrexsvw  3468  cbvralsv  3469  cbvrexsv  3470  cbvrabw  3489  cbvrab  3490  sbhypf  3552  mob2  3706  reu2  3716  reu6  3717  sbcralt  3855  sbcreu  3859  cbvrabcsfw  3924  cbvreucsf  3927  cbvrabcsf  3928  csbif  4522  cbvopab1  5139  cbvopab1g  5140  cbvopab1s  5142  cbvmptf  5165  cbvmptfg  5166  opelopabsb  5417  csbopab  5442  csbopabgALT  5443  opeliunxp  5619  ralxpf  5717  cbviotaw  6321  cbviota  6323  csbiota  6348  f1ossf1o  6890  cbvriotaw  7123  cbvriota  7127  csbriota  7129  onminex  7522  tfis  7569  findes  7612  abrexex2g  7665  opabex3d  7666  opabex3rd  7667  opabex3  7668  dfoprab4f  7754  uzind4s  12309  ac6sf2  30370  esumcvg  31345  wl-sb8t  34803  wl-sbalnae  34813  wl-ax11-lem8  34839  sbcrexgOLD  39431  scottabes  40627  pm13.193  40792  2reu8i  43361  opeliun2xp  44430