Theorem eqabri 2871

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109  {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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eqabcri  2872  rabid  3427  csbcow  3877  csbco  3878  csbgfi  3882  csbnestgfw  4385  csbnestgf  4390  ssrelOLD  5746  relopabi  5785  cnv0  6113  funcnv3  6586  opabiota  6943  zfrep6  7933  frrlem2  8266  frrlem3  8267  frrlem4  8268  frrlem8  8272  fprresex  8289  tfrlem4  8347  tfrlem8  8352  tfrlem9  8353  ixpn0  8903  sbthlem1  9051  dffi3  9382  1idpr  10982  ltexprlem1  10989  ltexprlem2  10990  ltexprlem3  10991  ltexprlem4  10992  ltexprlem6  10994  ltexprlem7  10995  reclem2pr  11001  reclem3pr  11002  reclem4pr  11003  supsrlem  11064  dissnref  23415  dissnlocfin  23416  txbas  23454  xkoccn  23506  xkoptsub  23541  xkoco1cn  23544  xkoco2cn  23545  xkoinjcn  23574  mbfi1fseqlem4  25619  avril1  30392  rnmposs  32598  bnj1436  34829  bnj916  34923  bnj983  34941  bnj1083  34968  bnj1245  35004  bnj1311  35014  bnj1371  35019  bnj1398  35024  setinds  35766  bj-elsngl  36956  bj-projun  36982  bj-projval  36984  f1omptsnlem  37324  icoreresf  37340  finxp0  37379  finxp1o  37380  finxpsuclem  37385  sdclem1  37737  csbcom2fi  38122  rr-grothshortbi  44292  modelaxreplem3  44970  upwordisword  46879  tworepnotupword  46884