Theorem eqabdv 2869

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqabcdv  2870  eqabi  2871  sbab  2882  rabeqcda  3410  iftrue  4485  iffalse  4488  dfopif  4826  iniseg  6056  setlikespec  6283  fncnvima2  7006  isoini  7284  dftpos3  8186  elecreseq  8684  mapsnd  8824  hartogslem1  9447  r1val2  9749  cardval2  9903  dfac3  10031  wrdval  14439  wrdnval  14468  submgmacs  18642  submacs  18752  ablsimpgfind  20041  dfrhm2  20410  lsppr  21045  rspsn  21288  znunithash  21519  tgval3  22907  txrest  23575  xkoptsub  23598  cnextf  24010  cnblcld  24718  shft2rab  25465  sca2rab  25469  renegscl  28494  grpoinvf  30607  elpjrn  32265  ofrn2  32718  ellcsrspsn  35835  neibastop3  36556  ec1cnvres  38469  ecun  38578  lkrval2  39350  lshpset2N  39379  hdmapoc  42191