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

Theorem eqabdv 2874
Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2156. (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 2078 . . 3 (𝜑 → ([𝑦 / 𝑥]𝑥𝐴 ↔ [𝑦 / 𝑥]𝜓))
3 clelsb1 2867 . . . 4 ([𝑦 / 𝑥]𝑥𝐴𝑦𝐴)
43bicomi 224 . . 3 (𝑦𝐴 ↔ [𝑦 / 𝑥]𝑥𝐴)
5 df-clab 2714 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
62, 4, 53bitr4g 314 . 2 (𝜑 → (𝑦𝐴𝑦 ∈ {𝑥𝜓}))
76eqrdv 2734 1 (𝜑𝐴 = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1539  [wsb 2063  wcel 2107  {cab 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815
This theorem is referenced by:  eqabcdv  2875  eqabi  2876  sbab  2888  rabeqcda  3447  iftrue  4530  iffalse  4533  dfopif  4869  iniseg  6114  setlikespec  6345  fncnvima2  7080  isoini  7359  dftpos3  8270  mapsnd  8927  hartogslem1  9583  r1val2  9878  cardval2  10032  dfac3  10162  wrdval  14556  wrdnval  14584  submgmacs  18731  submacs  18841  ablsimpgfind  20131  dfrhm2  20475  lsppr  21093  rspsn  21344  znunithash  21584  tgval3  22971  txrest  23640  xkoptsub  23663  cnextf  24075  cnblcld  24796  shft2rab  25544  sca2rab  25548  renegscl  28431  grpoinvf  30552  elpjrn  32210  ofrn2  32651  ellcsrspsn  35647  neibastop3  36364  ecres2  38281  lkrval2  39092  lshpset2N  39121  hdmapoc  41934
  Copyright terms: Public domain W3C validator