Theorem eqabdv 2872

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  [wsb 2073   ∈ wcel 2119  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eqabcdv  2873  eqabi  2874  sbab  2885  rabeqcda  3402  iftrue  4460  iffalse  4463  dfopif  4801  iniseg  6049  setlikespec  6276  fncnvima2  7002  isoini  7282  dftpos3  8184  elecreseq  8683  mapsnd  8824  hartogslem1  9447  r1val2  9752  cardval2  9906  dfac3  10034  wrdval  14469  wrdnval  14498  submgmacs  18676  submacs  18786  ablsimpgfind  20078  dfrhm2  20445  lsppr  21083  rspsn  21326  znunithash  21539  tgval3  22946  txrest  23614  xkoptsub  23637  cnextf  24049  cnblcld  24757  shft2rab  25493  sca2rab  25497  renegscl  28508  grpoinvf  30621  elpjrn  32279  ofrn2  32732  ellcsrspsn  35869  neibastop3  36590  ec1cnvres  38643  ecun  38760  disjimdmqseq  39176  lkrval2  39582  lshpset2N  39611  hdmapoc  42423