Theorem eqabri 2876

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 2875	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	mptru 1548	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 206   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113  {cab 2711

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-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eqabcri  2877  rabid  3418  csbcow  3862  csbco  3863  csbgfi  3867  csbnestgfw  4373  csbnestgf  4378  relopabi  5769  cnv0OLD  6095  funcnv3  6559  opabiota  6913  zfrep6  7896  frrlem2  8226  frrlem3  8227  frrlem4  8228  frrlem8  8232  fprresex  8249  tfrlem4  8307  tfrlem8  8312  tfrlem9  8313  ixpn0  8863  sbthlem1  9010  dffi3  9325  setinds  9649  1idpr  10930  ltexprlem1  10937  ltexprlem2  10938  ltexprlem3  10939  ltexprlem4  10940  ltexprlem6  10942  ltexprlem7  10943  reclem2pr  10949  reclem3pr  10950  reclem4pr  10951  supsrlem  11012  dissnref  23453  dissnlocfin  23454  txbas  23492  xkoccn  23544  xkoptsub  23579  xkoco1cn  23582  xkoco2cn  23583  xkoinjcn  23612  mbfi1fseqlem4  25656  avril1  30454  rnmposs  32667  bnj1436  34862  bnj916  34956  bnj983  34974  bnj1083  35001  bnj1245  35037  bnj1311  35047  bnj1371  35052  bnj1398  35057  tz9.1regs  35141  bj-elsngl  37023  bj-projun  37049  bj-projval  37051  f1omptsnlem  37391  icoreresf  37407  finxp0  37446  finxp1o  37447  finxpsuclem  37452  sdclem1  37793  csbcom2fi  38178  rr-grothshortbi  44410  modelaxreplem3  45087