Theorem sbequ12 2109

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

Syntax hints:   → wi 4   ↔ wb 196  [wsb 1878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-sb 1879

This theorem is referenced by:  sbequ12r  2110  sbequ12a  2111  axc16ALT  2364  nfsb4t  2387  sbco2  2413  sb8  2422  sb8e  2423  sbal1  2458  clelab  2746  sbab  2748  cbvralf  3160  cbvralsv  3177  cbvrexsv  3178  cbvrab  3193  sbhypf  3248  mob2  3380  reu2  3388  reu6  3389  sbcralt  3504  sbcreu  3509  cbvreucsf  3560  cbvrabcsf  3561  csbif  4129  cbvopab1  4714  cbvopab1s  4716  cbvmptf  4739  cbvmpt  4740  opelopabsb  4975  csbopab  4998  csbopabgALT  4999  opeliunxp  5160  ralxpf  5257  cbviota  5844  csbiota  5869  cbvriota  6606  csbriota  6608  onminex  6992  tfis  7039  findes  7081  abrexex2g  7129  opabex3d  7130  opabex3  7131  abrexex2OLD  7135  dfoprab4f  7211  uzind4s  11733  ac6sf2  29401  esumcvg  30122  bj-sbab  32759  wl-sb8t  33304  wl-sbalnae  33316  wl-ax11-lem8  33340  sbcrexgOLD  37168  pm13.193  38432  opeliun2xp  41876