Theorem sbequ12 2290

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  [wsb 2101

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102

This theorem is used by:  sbequ12r  2291  sbequ12a  2293  sb8ef  2387  sbbib  2393  axc16ALT  2521  nfsb4t  2531  sbco2  2543  sb8  2549  sb8e  2550  sbal1  2560  sbal2  2561  sbab  2910  cbvrexsvw  3318  cbvralf  3349  cbvralsv  3355  cbvrexsv  3356  cbvrab  3453  mob2  3676  reu2  3686  reu6  3687  sbcralt  3823  sbcreu  3827  cbvrabcsfw  3892  cbvreucsf  3895  cbvrabcsf  3896  csbif  4543  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvmptf  5211  cbvmptfg  5212  csbopab  5537  csbopabw  5538  opeliunxp  5725  opeliun2xp  5726  ralxpf  5834  cbviotaw  6527  cbviota  6529  csbiota  6559  f1ossf1o  7161  cbvriotaw  7417  cbvriota  7421  csbriota  7423  onminex  7850  tfis  7900  findes  7946  abrexex2g  8010  opabex3d  8011  opabex3rd  8012  opabex3  8013  dfoprab4f  8102  scottabes  9978  uzind4s  13075  ac6sf2  33314  esumcvg  34829  reu6f  35820  regsfromsetind  37542  wl-sb8t  38752  wl-sbalnae  38762  pm13.193  45656  2reu8i  48457  ichnfimlem  48818