Theorem eqabri 2907

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

Syntax hints:   ↔ wb 209   = wceq 1563  ⊤wtru 1564   ∈ wcel 2145  {cab 2743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840

This theorem is referenced by:  eqabcri  2908  rabid  3438  csbcow  3870  csbco  3871  csbgfi  3875  csbnestgfw  4379  csbnestgf  4384  relopabi  5799  cnv0OLD  5860  funcnv3  6595  opabiota  6953  zfrep6OLD  7940  frrlem2  8272  frrlem3  8273  frrlem4  8274  frrlem8  8278  fprresex  8295  tfrlem4  8353  tfrlem8  8359  tfrlem9  8360  ixpn0  8916  sbthlem1  9063  dffi3  9379  setinds  9706  1idpr  11002  ltexprlem1  11009  ltexprlem2  11010  ltexprlem3  11011  ltexprlem4  11012  ltexprlem6  11014  ltexprlem7  11015  reclem2pr  11021  reclem3pr  11022  reclem4pr  11023  supsrlem  11084  dissnref  23642  dissnlocfin  23643  txbas  23681  xkoccn  23733  xkoptsub  23768  xkoco1cn  23771  xkoco2cn  23772  xkoinjcn  23801  mbfi1fseqlem4  25834  avril1  30719  rnmposs  32926  bnj1436  35139  bnj916  35233  bnj983  35251  bnj1083  35278  bnj1245  35314  bnj1311  35324  bnj1371  35329  bnj1398  35334  tz9.1regs  35437  bj-elsngl  37460  bj-projun  37486  bj-projval  37488  f1omptsnlem  37837  icoreresf  37853  finxp0  37892  finxp1o  37893  finxpsuclem  37898  sdclem1  38249  csbcom2fi  38634  ralrnmo  38867  raldmqsmo  38869  rr-grothshortbi  44872  modelaxreplem3  45548