Theorem eqabdv 2898

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2146  {cab 2743

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is used by:  eqabcdv  2899  eqabi  2900  sbab  2911  rabeqcda  3429  iftrue  4495  iffalse  4498  dfopif  4837  iniseg  6101  setlikespec  6330  fncnvima2  7060  isoini  7345  dftpos3  8246  elecreseq  8750  mapsnd  8890  hartogslem1  9511  r1val2  9816  cardval2  9993  dfac3  10121  wrdval  14571  wrdnval  14600  submgmacs  18807  submacs  18923  ablsimpgfind  20226  dfrhm2  20602  lsppr  21264  rspsn  21551  znunithash  21764  tgval3  23170  txrest  23839  xkoptsub  23862  cnextf  24274  cnblcld  24982  shft2rab  25718  sca2rab  25722  renegscl  28742  grpoinvf  30955  elpjrn  32613  ofrn2  33056  ellcsrspsn  36170  neibastop3  36930  ec1cnvres  38983  ecun  39100  disjimdmqseq  39516  lkrval2  39922  lshpset2N  39951  hdmapoc  42763