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

Theorem sbc2ie 3503
 Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008.) (Revised by Mario Carneiro, 19-Dec-2013.)
Hypotheses
Ref Expression
sbc2ie.1 𝐴 ∈ V
sbc2ie.2 𝐵 ∈ V
sbc2ie.3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
Assertion
Ref Expression
sbc2ie ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝜓)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝜓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)

Proof of Theorem sbc2ie
StepHypRef Expression
1 sbc2ie.1 . 2 𝐴 ∈ V
2 sbc2ie.2 . 2 𝐵 ∈ V
3 nfv 1842 . . 3 𝑥𝜓
4 nfv 1842 . . 3 𝑦𝜓
52nfth 1726 . . 3 𝑥 𝐵 ∈ V
6 sbc2ie.3 . . 3 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
73, 4, 5, 6sbc2iegf 3502 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝜓))
81, 2, 7mp2an 708 1 ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1482   ∈ wcel 1989  Vcvv 3198  [wsbc 3433 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-12 2046  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3200  df-sbc 3434 This theorem is referenced by:  sbc3ie  3505  brfi1uzind  13275  opfi1uzind  13278  brfi1uzindOLD  13281  opfi1uzindOLD  13284  wrd2ind  13471  isprs  16924  isdrs  16928  istos  17029  issrg  18501  isslmd  29740  rexrabdioph  37184  rmydioph  37407  rmxdioph  37409  expdiophlem2  37415
 Copyright terms: Public domain W3C validator