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 2065

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 2008  ax-12 2178

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

This theorem is referenced by:  sbequ12r  2253  sbequ12a  2255  sb8fOLD  2353  sb8ef  2354  sbbib  2360  axc16ALT  2488  nfsb4t  2498  sbco2  2510  sb8  2516  sb8e  2517  sbal1  2527  sbal2  2528  sbab  2876  cbvrexsvw  3293  cbvralsvwOLD  3294  cbvralsvwOLDOLD  3295  cbvrexsvwOLD  3296  cbvralf  3336  cbvralsv  3342  cbvrexsv  3343  cbvrabwOLD  3445  cbvrab  3449  sbhypfOLD  3514  mob2  3689  reu2  3699  reu6  3700  sbcralt  3838  sbcreu  3842  cbvrabcsfw  3906  cbvreucsf  3909  cbvrabcsf  3910  csbif  4549  cbvopab1  5184  cbvopab1g  5185  cbvopab1s  5187  cbvmptf  5210  cbvmptfg  5211  csbopab  5518  csbopabgALT  5519  opeliunxp  5708  opeliun2xp  5709  ralxpf  5813  cbviotaw  6474  cbviota  6476  csbiota  6507  f1ossf1o  7103  cbvriotaw  7356  cbvriota  7360  csbriota  7362  onminex  7781  tfis  7834  findes  7879  abrexex2g  7946  opabex3d  7947  opabex3rd  7948  opabex3  7949  dfoprab4f  8038  uzind4s  12874  ac6sf2  32555  esumcvg  34083  wl-sb8t  37547  wl-sbalnae  37557  wl-ax11-lem8  37587  sbcrexgOLD  42780  scottabes  44238  pm13.193  44407  2reu8i  47118  ichnfimlem  47468