Theorem eqabri 2905

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

Syntax hints:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eqabcri  2906  rabid  3437  csbcow  3869  csbco  3870  csbgfi  3874  csbnestgfw  4388  csbnestgf  4393  relopabi  5811  cnv0OLD  5872  funcnv3  6608  opabiota  6965  zfrep6OLD  7953  frrlem2  8285  frrlem3  8286  frrlem4  8287  frrlem8  8291  fprresex  8308  tfrlem4  8366  tfrlem8  8372  tfrlem9  8373  ixpn0  8929  sbthlem1  9076  dffi3  9392  setinds  9719  1idpr  11015  ltexprlem1  11022  ltexprlem2  11023  ltexprlem3  11024  ltexprlem4  11025  ltexprlem6  11027  ltexprlem7  11028  reclem2pr  11034  reclem3pr  11035  reclem4pr  11036  supsrlem  11097  dissnref  23666  dissnlocfin  23667  txbas  23705  xkoccn  23757  xkoptsub  23792  xkoco1cn  23795  xkoco2cn  23796  xkoinjcn  23825  mbfi1fseqlem4  25858  avril1  30795  rnmposs  32999  bnj1436  35208  bnj916  35302  bnj983  35320  bnj1083  35347  bnj1245  35383  bnj1311  35393  bnj1371  35398  bnj1398  35403  tz9.1regs  35528  bj-elsngl  37585  bj-projun  37611  bj-projval  37613  f1omptsnlem  37963  icoreresf  37979  finxp0  38018  finxp1o  38019  finxpsuclem  38024  sdclem1  38375  csbcom2fi  38758  ralrnmo  38991  raldmqsmo  38993  rr-grothshortbi  44996  modelaxreplem3  45672