Theorem eqabri 2879

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

Syntax hints:   ↔ wb 206   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eqabcri  2880  rabid  3411  csbcow  3853  csbco  3854  csbgfi  3858  csbnestgfw  4363  csbnestgf  4368  relopabi  5771  cnv0OLD  6098  funcnv3  6562  opabiota  6916  zfrep6OLD  7901  frrlem2  8230  frrlem3  8231  frrlem4  8232  frrlem8  8236  fprresex  8253  tfrlem4  8311  tfrlem8  8316  tfrlem9  8317  ixpn0  8871  sbthlem1  9018  dffi3  9337  setinds  9661  1idpr  10943  ltexprlem1  10950  ltexprlem2  10951  ltexprlem3  10952  ltexprlem4  10953  ltexprlem6  10955  ltexprlem7  10956  reclem2pr  10962  reclem3pr  10963  reclem4pr  10964  supsrlem  11025  dissnref  23503  dissnlocfin  23504  txbas  23542  xkoccn  23594  xkoptsub  23629  xkoco1cn  23632  xkoco2cn  23633  xkoinjcn  23662  mbfi1fseqlem4  25695  avril1  30548  rnmposs  32761  bnj1436  34997  bnj916  35091  bnj983  35109  bnj1083  35136  bnj1245  35172  bnj1311  35182  bnj1371  35187  bnj1398  35192  tz9.1regs  35294  bj-elsngl  37291  bj-projun  37317  bj-projval  37319  f1omptsnlem  37666  icoreresf  37682  finxp0  37721  finxp1o  37722  finxpsuclem  37727  sdclem1  38078  csbcom2fi  38463  ralrnmo  38696  raldmqsmo  38698  rr-grothshortbi  44748  modelaxreplem3  45425