Theorem sbequ12 2259

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

Syntax hints:   → wi 4   ↔ wb 206  [wsb 2068

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 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  sbequ12r  2260  sbequ12a  2262  sb8ef  2360  sbbib  2366  axc16ALT  2494  nfsb4t  2504  sbco2  2516  sb8  2522  sb8e  2523  sbal1  2533  sbal2  2534  sbab  2883  cbvrexsvw  3290  cbvralsvwOLD  3291  cbvralf  3323  cbvralsv  3329  cbvrexsv  3330  cbvrabwOLD  3426  cbvrab  3429  mob2  3662  reu2  3672  reu6  3673  sbcralt  3811  sbcreu  3815  cbvrabcsfw  3879  cbvreucsf  3882  cbvrabcsf  3883  csbif  4525  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvmptf  5186  cbvmptfg  5187  csbopab  5503  csbopabgALT  5504  opeliunxp  5691  opeliun2xp  5692  ralxpf  5795  cbviotaw  6455  cbviota  6457  csbiota  6485  f1ossf1o  7075  cbvriotaw  7326  cbvriota  7330  csbriota  7332  onminex  7749  tfis  7799  findes  7844  abrexex2g  7910  opabex3d  7911  opabex3rd  7912  opabex3  7913  dfoprab4f  8002  uzind4s  12849  ac6sf2  32710  esumcvg  34246  regsfromsetind  36737  wl-sb8t  37891  wl-sbalnae  37901  sbcrexgOLD  43231  scottabes  44687  pm13.193  44856  2reu8i  47573  ichnfimlem  47935