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  3422  csbcow  3866  csbco  3867  csbgfi  3871  csbnestgfw  4376  csbnestgf  4381  relopabi  5779  cnv0OLD  6106  funcnv3  6570  opabiota  6924  zfrep6  7909  frrlem2  8239  frrlem3  8240  frrlem4  8241  frrlem8  8245  fprresex  8262  tfrlem4  8320  tfrlem8  8325  tfrlem9  8326  ixpn0  8880  sbthlem1  9027  dffi3  9346  setinds  9670  1idpr  10952  ltexprlem1  10959  ltexprlem2  10960  ltexprlem3  10961  ltexprlem4  10962  ltexprlem6  10964  ltexprlem7  10965  reclem2pr  10971  reclem3pr  10972  reclem4pr  10973  supsrlem  11034  dissnref  23484  dissnlocfin  23485  txbas  23523  xkoccn  23575  xkoptsub  23610  xkoco1cn  23613  xkoco2cn  23614  xkoinjcn  23643  mbfi1fseqlem4  25687  avril1  30550  rnmposs  32762  bnj1436  35014  bnj916  35108  bnj983  35126  bnj1083  35153  bnj1245  35189  bnj1311  35199  bnj1371  35204  bnj1398  35209  tz9.1regs  35309  bj-elsngl  37213  bj-projun  37239  bj-projval  37241  f1omptsnlem  37588  icoreresf  37604  finxp0  37643  finxp1o  37644  finxpsuclem  37649  sdclem1  37991  csbcom2fi  38376  ralrnmo  38609  raldmqsmo  38611  rr-grothshortbi  44656  modelaxreplem3  45333