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

Theorem eqabdv 2868
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2155. (Revised by Wolf Lammen, 6-May-2023.)
Hypothesis
Ref Expression
eqabdv.1 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
eqabdv (𝜑𝐴 = {𝑥𝜓})
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem eqabdv
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqabdv.1 . . . 4 (𝜑 → (𝑥𝐴𝜓))
21sbbidv 2083 . . 3 (𝜑 → ([𝑦 / 𝑥]𝑥𝐴 ↔ [𝑦 / 𝑥]𝜓))
3 clelsb1 2861 . . . 4 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
43bicomi 223 . . 3 (𝑦𝐴 ↔ [𝑦 / 𝑥]𝑥𝐴)
5 df-clab 2711 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
62, 4, 53bitr4g 314 . 2 (𝜑 → (𝑦𝐴𝑦 ∈ {𝑥𝜓}))
76eqrdv 2731 1 (𝜑𝐴 = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  [wsb 2068  wcel 2107  {cab 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811
This theorem is referenced by:  eqabcdv  2869  eqabi  2870  sbab  2883  rabeqcda  3444  iftrue  4533  iffalse  4536  dfopif  4869  iniseg  6093  setlikespec  6323  fncnvima2  7058  isoini  7330  dftpos3  8224  mapsnd  8876  hartogslem1  9533  r1val2  9828  cardval2  9982  dfac3  10112  wrdval  14463  wrdnval  14491  submacs  18704  ablsimpgfind  19972  dfrhm2  20242  lsppr  20692  rspsn  20879  znunithash  21104  tgval3  22448  txrest  23117  xkoptsub  23140  cnextf  23552  cnblcld  24273  shft2rab  25007  sca2rab  25011  grpoinvf  29763  elpjrn  31421  ofrn2  31843  neibastop3  35185  ecres2  37085  lkrval2  37898  lshpset2N  37927  hdmapoc  40740  submgmacs  46509
  Copyright terms: Public domain W3C validator