Theorem eqabri 2875

Description: Equality of a class variable and a class abstraction (inference form). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)

Hypothesis

Ref	Expression
eqabri.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
eqabri	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem eqabri

Step	Hyp	Ref	Expression
1		eqabri.1	. . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
3	2	eqabrd 2874	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1546	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 205   = wceq 1539  ⊤wtru 1540   ∈ wcel 2104  {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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eqabcri  2876  rabid  3450  csbcow  3909  csbco  3910  csbgfi  3915  csbnestgfw  4420  csbnestgf  4425  ssrelOLD  5784  relopabi  5823  cnv0  6141  funcnv3  6619  opabiota  6975  zfrep6  7945  frrlem2  8276  frrlem3  8277  frrlem4  8278  frrlem8  8282  fprresex  8299  wfrlem2OLD  8313  wfrlem3OLD  8314  wfrlem4OLD  8316  wfrdmclOLD  8321  tfrlem4  8383  tfrlem8  8388  tfrlem9  8389  ixpn0  8928  sbthlem1  9087  dffi3  9430  1idpr  11028  ltexprlem1  11035  ltexprlem2  11036  ltexprlem3  11037  ltexprlem4  11038  ltexprlem6  11040  ltexprlem7  11041  reclem2pr  11047  reclem3pr  11048  reclem4pr  11049  supsrlem  11110  dissnref  23254  dissnlocfin  23255  txbas  23293  xkoccn  23345  xkoptsub  23380  xkoco1cn  23383  xkoco2cn  23384  xkoinjcn  23413  mbfi1fseqlem4  25470  avril1  29981  rnmposs  32164  bnj1436  34146  bnj916  34240  bnj983  34258  bnj1083  34285  bnj1245  34321  bnj1311  34331  bnj1371  34336  bnj1398  34341  setinds  35052  bj-elsngl  36154  bj-projun  36180  bj-projval  36182  f1omptsnlem  36522  icoreresf  36538  finxp0  36577  finxp1o  36578  finxpsuclem  36583  sdclem1  36916  csbcom2fi  37301  rr-grothshortbi  43366  upwordisword  45895  tworepnotupword  45900