Theorem eqabdv 2861

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqabcdv  2862  eqabi  2863  sbab  2875  rabeqcda  3417  iftrue  4494  iffalse  4497  dfopif  4834  iniseg  6068  setlikespec  6298  fncnvima2  7033  isoini  7313  dftpos3  8223  elecreseq  8720  mapsnd  8859  hartogslem1  9495  r1val2  9790  cardval2  9944  dfac3  10074  wrdval  14481  wrdnval  14510  submgmacs  18644  submacs  18754  ablsimpgfind  20042  dfrhm2  20383  lsppr  21000  rspsn  21243  znunithash  21474  tgval3  22850  txrest  23518  xkoptsub  23541  cnextf  23953  cnblcld  24662  shft2rab  25409  sca2rab  25413  renegscl  28349  grpoinvf  30461  elpjrn  32119  ofrn2  32564  ellcsrspsn  35628  neibastop3  36350  lkrval2  39083  lshpset2N  39112  hdmapoc  41925