Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  elab2g GIF version

Theorem elab2g 2711
 Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1 (𝑥 = 𝐴 → (𝜑𝜓))
elab2g.2 𝐵 = {𝑥𝜑}
Assertion
Ref Expression
elab2g (𝐴𝑉 → (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3 𝐵 = {𝑥𝜑}
21eleq2i 2120 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 2710 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 185 1 (𝐴𝑉 → (𝐴𝐵𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102   = wceq 1259   ∈ wcel 1409  {cab 2042 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576 This theorem is referenced by:  elab2  2712  elab4g  2713  eldif  2954  elun  3111  elin  3153  elsng  3417  elprg  3422  eluni  3610  eliun  3688  eliin  3689  elopab  4022  elong  4137  opeliunxp  4422  elrn2g  4552  eldmg  4557  elrnmpt  4610  elrnmpt1  4612  elimag  4699  elrnmpt2g  5640  eloprabi  5849  tfrlem3ag  5954  elqsg  6186  1idprl  6745  1idpru  6746  recexprlemell  6777  recexprlemelu  6778
 Copyright terms: Public domain W3C validator