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

Theorem sbcie 3830
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 3828 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑𝜓))
41, 3ax-mp 5 1 ([𝐴 / 𝑥]𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  Vcvv 3480  [wsbc 3788
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-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3789
This theorem is referenced by:  sbc2ie  3866  csbie  3934  rexopabb  5533  reuop  6313  tfinds2  7885  soseq  8184  findcard2  9204  ac6sfi  9320  ac6num  10519  fpwwe  10686  nn1suc  12288  wrdind  14760  cjth  15142  fprodser  15985  prmind2  16722  joinlem  18428  meetlem  18442  mndind  18841  isghm  19233  isghmOLD  19234  islmod  20862  islindf  21832  fgcl  23886  cfinfil  23901  csdfil  23902  supfil  23903  fin1aufil  23940  quotval  26334  dfconngr1  30207  isconngr  30208  isconngr1  30209  wrdt2ind  32938  bnj62  34734  bnj610  34761  bnj976  34791  bnj106  34882  bnj125  34886  bnj154  34892  bnj155  34893  bnj526  34902  bnj540  34906  bnj591  34925  bnj609  34931  bnj893  34942  bnj1417  35055  poimirlem27  37654  sdclem2  37749  fdc  37752  fdc1  37753  lshpkrlem3  39113  hdmap1fval  41798  hdmapfval  41829  sn-isghm  42683  rabren3dioph  42826  2nn0ind  42957  zindbi  42958  onfrALTlem5  44562  onfrALTlem5VD  44905  reupr  47509
  Copyright terms: Public domain W3C validator