Theorem sbequ12 2252

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 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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

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

This theorem is referenced by:  sbequ12r  2253  sbequ12a  2255  sb5OLD  2278  sb8fOLD  2360  sb8ef  2361  sbbib  2367  axc16ALT  2497  nfsb4t  2507  sbco2  2519  sb8  2525  sb8e  2526  sbal1  2536  sbal2  2537  sbab  2892  nfabdwOLD  2933  cbvrexsvw  3324  cbvralsvwOLD  3325  cbvralsvwOLDOLD  3326  cbvrexsvwOLD  3327  cbvralf  3368  cbvralsv  3374  cbvrexsv  3375  cbvrabwOLD  3482  cbvrab  3487  sbhypfOLD  3557  mob2  3737  reu2  3747  reu6  3748  sbcralt  3894  sbcreu  3898  cbvrabcsfw  3965  cbvreucsf  3968  cbvrabcsf  3969  csbif  4605  cbvopab1  5241  cbvopab1g  5242  cbvopab1s  5244  cbvmptf  5275  cbvmptfg  5276  csbopab  5574  csbopabgALT  5575  opeliunxp  5767  ralxpf  5871  cbviotaw  6532  cbviota  6535  csbiota  6566  f1ossf1o  7162  cbvriotaw  7413  cbvriota  7418  csbriota  7420  onminex  7838  tfis  7892  findes  7940  abrexex2g  8005  opabex3d  8006  opabex3rd  8007  opabex3  8008  dfoprab4f  8097  uzind4s  12973  ac6sf2  32644  esumcvg  34050  wl-sb8t  37506  wl-sbalnae  37516  wl-ax11-lem8  37546  sbcrexgOLD  42741  scottabes  44211  pm13.193  44380  2reu8i  47028  ichnfimlem  47337  opeliun2xp  48057