Theorem eqabdv 2902

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994.) Avoid ax-11 2198. (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 2119	. . 3 ⊢ (𝜑 → ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝜓))
3		clelsb1 2896	. . . 4 ⊢ ([𝑦 / 𝑥]𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
4	3	bicomi 227	. . 3 ⊢ (𝑦 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑥 ∈ 𝐴)
5		df-clab 2748	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
6	2, 4, 5	3bitr4g 317	. 2 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
7	6	eqrdv 2767	1 ⊢ (𝜑 → 𝐴 = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  [wsb 2097   ∈ wcel 2149  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eqabcdv  2903  eqabi  2904  sbab  2915  rabeqcda  3434  iftrue  4495  iffalse  4498  dfopif  4836  iniseg  6097  setlikespec  6324  fncnvima2  7054  isoini  7334  dftpos3  8236  elecreseq  8740  mapsnd  8880  hartogslem1  9500  r1val2  9805  cardval2  9973  dfac3  10101  wrdval  14549  wrdnval  14578  submgmacs  18771  submacs  18882  ablsimpgfind  20178  dfrhm2  20552  lsppr  21188  rspsn  21466  znunithash  21679  tgval3  23085  txrest  23753  xkoptsub  23776  cnextf  24188  cnblcld  24896  shft2rab  25632  sca2rab  25636  renegscl  28653  grpoinvf  30821  elpjrn  32479  ofrn2  32922  ellcsrspsn  36028  neibastop3  36758  ec1cnvres  38810  ecun  38927  disjimdmqseq  39343  lkrval2  39749  lshpset2N  39778  hdmapoc  42590