Theorem eqabdv 2893

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

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

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  eqabcdv  2894  eqabi  2895  sbab  2906  rabeqcda  3423  iftrue  4488  iffalse  4491  dfopif  4830  iniseg  6093  setlikespec  6323  fncnvima2  7053  isoini  7339  dftpos3  8242  elecreseq  8746  mapsnd  8893  hartogslem1  9514  r1val2  9819  cardval2  9996  dfac3  10124  wrdval  14581  wrdnval  14610  submgmacs  18819  submacs  18936  ablsimpgfind  20239  dfrhm2  20615  lsppr  21277  rspsn  21564  znunithash  21777  tgval3  23188  txrest  23857  xkoptsub  23880  cnextf  24292  cnblcld  25000  shft2rab  25736  sca2rab  25740  renegscl  28763  grpoinvf  31013  elpjrn  32671  ofrn2  33113  ellcsrspsn  36220  neibastop3  36981  ec1cnvres  39024  ecun  39141  disjimdmqseq  39557  lkrval2  39963  lshpset2N  39992  hdmapoc  42804