Theorem eqabri 2878

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

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

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 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqabcri  2879  rabid  3420  csbcow  3864  csbco  3865  csbgfi  3869  csbnestgfw  4374  csbnestgf  4379  relopabi  5771  cnv0OLD  6098  funcnv3  6562  opabiota  6916  zfrep6  7899  frrlem2  8229  frrlem3  8230  frrlem4  8231  frrlem8  8235  fprresex  8252  tfrlem4  8310  tfrlem8  8315  tfrlem9  8316  ixpn0  8868  sbthlem1  9015  dffi3  9334  setinds  9658  1idpr  10940  ltexprlem1  10947  ltexprlem2  10948  ltexprlem3  10949  ltexprlem4  10950  ltexprlem6  10952  ltexprlem7  10953  reclem2pr  10959  reclem3pr  10960  reclem4pr  10961  supsrlem  11022  dissnref  23472  dissnlocfin  23473  txbas  23511  xkoccn  23563  xkoptsub  23598  xkoco1cn  23601  xkoco2cn  23602  xkoinjcn  23631  mbfi1fseqlem4  25675  avril1  30538  rnmposs  32752  bnj1436  34995  bnj916  35089  bnj983  35107  bnj1083  35134  bnj1245  35170  bnj1311  35180  bnj1371  35185  bnj1398  35190  tz9.1regs  35290  bj-elsngl  37169  bj-projun  37195  bj-projval  37197  f1omptsnlem  37541  icoreresf  37557  finxp0  37596  finxp1o  37597  finxpsuclem  37602  sdclem1  37944  csbcom2fi  38329  rr-grothshortbi  44544  modelaxreplem3  45221