Theorem eqabri 2882

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

Syntax hints:   ↔ wb 207   = wceq 1547  ⊤wtru 1548   ∈ wcel 2119  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815

This theorem is referenced by:  eqabcri  2883  rabid  3413  csbcow  3853  csbco  3854  csbgfi  3858  csbnestgfw  4357  csbnestgf  4362  relopabi  5772  cnv0OLD  6098  funcnv3  6562  opabiota  6916  zfrep6OLD  7904  frrlem2  8234  frrlem3  8235  frrlem4  8236  frrlem8  8240  fprresex  8257  tfrlem4  8315  tfrlem8  8320  tfrlem9  8321  ixpn0  8875  sbthlem1  9022  dffi3  9341  setinds  9668  1idpr  10950  ltexprlem1  10957  ltexprlem2  10958  ltexprlem3  10959  ltexprlem4  10960  ltexprlem6  10962  ltexprlem7  10963  reclem2pr  10969  reclem3pr  10970  reclem4pr  10971  supsrlem  11032  dissnref  23518  dissnlocfin  23519  txbas  23557  xkoccn  23609  xkoptsub  23644  xkoco1cn  23647  xkoco2cn  23648  xkoinjcn  23677  mbfi1fseqlem4  25710  avril1  30558  rnmposs  32772  bnj1436  35028  bnj916  35122  bnj983  35140  bnj1083  35167  bnj1245  35203  bnj1311  35213  bnj1371  35218  bnj1398  35223  tz9.1regs  35322  bj-elsngl  37328  bj-projun  37354  bj-projval  37356  f1omptsnlem  37705  icoreresf  37721  finxp0  37760  finxp1o  37761  finxpsuclem  37766  sdclem1  38117  csbcom2fi  38502  ralrnmo  38735  raldmqsmo  38737  rr-grothshortbi  44754  modelaxreplem3  45431