Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcie Structured version   Visualization version   GIF version

Theorem sbcie 3437
 Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 4-Sep-2004.)
Hypotheses
Ref Expression
sbcie.1 𝐴 ∈ V
sbcie.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
sbcie ([𝐴 / 𝑥]𝜑𝜓)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbcie
StepHypRef Expression
1 sbcie.1 . 2 𝐴 ∈ V
2 sbcie.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32sbcieg 3435 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑𝜓))
41, 3ax-mp 5 1 ([𝐴 / 𝑥]𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977  Vcvv 3173  [wsbc 3402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175  df-sbc 3403 This theorem is referenced by:  tfinds2  6955  findcard2  8085  ac6sfi  8089  ac6num  9184  fpwwe  9347  nn1suc  10918  wrdind  13328  cjth  13691  fprodser  14518  prmind2  15236  joinlem  16834  meetlem  16848  mrcmndind  17189  isghm  17483  islmod  18690  islindf  19970  fgcl  21492  cfinfil  21507  csdfil  21508  supfil  21509  fin1aufil  21546  quotval  23851  bnj62  30040  bnj610  30071  bnj976  30102  bnj106  30192  bnj125  30196  bnj154  30202  bnj155  30203  bnj526  30212  bnj540  30216  bnj591  30235  bnj609  30241  bnj893  30252  bnj1417  30363  soseq  30995  poimirlem27  32606  sdclem2  32708  fdc  32711  fdc1  32712  lshpkrlem3  33417  hdmap1fval  36104  hdmapfval  36137  rabren3dioph  36397  2nn0ind  36528  zindbi  36529  onfrALTlem5  37778  dfconngr1  41355  isconngr  41356  isconngr1  41357
 Copyright terms: Public domain W3C validator