Theorem eqabri 2875

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

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

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 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eqabcri  2876  rabid  3417  csbcow  3861  csbco  3862  csbgfi  3866  csbnestgfw  4371  csbnestgf  4376  relopabi  5768  cnv0OLD  6094  funcnv3  6558  opabiota  6912  zfrep6  7895  frrlem2  8225  frrlem3  8226  frrlem4  8227  frrlem8  8231  fprresex  8248  tfrlem4  8306  tfrlem8  8311  tfrlem9  8312  ixpn0  8862  sbthlem1  9009  dffi3  9324  setinds  9648  1idpr  10929  ltexprlem1  10936  ltexprlem2  10937  ltexprlem3  10938  ltexprlem4  10939  ltexprlem6  10941  ltexprlem7  10942  reclem2pr  10948  reclem3pr  10949  reclem4pr  10950  supsrlem  11011  dissnref  23446  dissnlocfin  23447  txbas  23485  xkoccn  23537  xkoptsub  23572  xkoco1cn  23575  xkoco2cn  23576  xkoinjcn  23605  mbfi1fseqlem4  25649  avril1  30447  rnmposs  32660  bnj1436  34874  bnj916  34968  bnj983  34986  bnj1083  35013  bnj1245  35049  bnj1311  35059  bnj1371  35064  bnj1398  35069  tz9.1regs  35153  bj-elsngl  37035  bj-projun  37061  bj-projval  37063  f1omptsnlem  37403  icoreresf  37419  finxp0  37458  finxp1o  37459  finxpsuclem  37464  sdclem1  37806  csbcom2fi  38191  rr-grothshortbi  44423  modelaxreplem3  45100