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.

Step	Hyp	Ref	Expression
1		eqabdv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝜓))
2	1	sbbidv 2078	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓))
3		clelsb1 2867	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 224	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2714	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 314	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2734	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

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