Theorem sbequ12 2251

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 2248	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑))
2		sbequ2 2249	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

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

This theorem is referenced by:  sbequ12r  2252  sbequ12a  2254  sb8fOLD  2356  sb8ef  2357  sbbib  2363  axc16ALT  2493  nfsb4t  2503  sbco2  2515  sb8  2521  sb8e  2522  sbal1  2532  sbal2  2533  sbab  2882  cbvrexsvw  3297  cbvralsvwOLD  3298  cbvralsvwOLDOLD  3299  cbvrexsvwOLD  3300  cbvralf  3339  cbvralsv  3345  cbvrexsv  3346  cbvrabwOLD  3453  cbvrab  3458  sbhypfOLD  3524  mob2  3698  reu2  3708  reu6  3709  sbcralt  3847  sbcreu  3851  cbvrabcsfw  3915  cbvreucsf  3918  cbvrabcsf  3919  csbif  4558  cbvopab1  5193  cbvopab1g  5194  cbvopab1s  5196  cbvmptf  5221  cbvmptfg  5222  csbopab  5530  csbopabgALT  5531  opeliunxp  5721  opeliun2xp  5722  ralxpf  5826  cbviotaw  6491  cbviota  6493  csbiota  6524  f1ossf1o  7118  cbvriotaw  7371  cbvriota  7375  csbriota  7377  onminex  7796  tfis  7850  findes  7896  abrexex2g  7963  opabex3d  7964  opabex3rd  7965  opabex3  7966  dfoprab4f  8055  uzind4s  12924  ac6sf2  32602  esumcvg  34117  wl-sb8t  37570  wl-sbalnae  37580  wl-ax11-lem8  37610  sbcrexgOLD  42808  scottabes  44266  pm13.193  44435  2reu8i  47142  ichnfimlem  47477