Theorem eqabri 2903

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

Syntax hints:   ↔ wb 208   = wceq 1559  ⊤wtru 1560   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  eqabcri  2904  rabid  3434  csbcow  3865  csbco  3866  csbgfi  3870  csbnestgfw  4373  csbnestgf  4378  relopabi  5791  cnv0OLD  5852  funcnv3  6585  opabiota  6943  zfrep6OLD  7930  frrlem2  8261  frrlem3  8262  frrlem4  8263  frrlem8  8267  fprresex  8284  tfrlem4  8342  tfrlem8  8348  tfrlem9  8349  ixpn0  8905  sbthlem1  9052  dffi3  9370  setinds  9697  1idpr  10980  ltexprlem1  10987  ltexprlem2  10988  ltexprlem3  10989  ltexprlem4  10990  ltexprlem6  10992  ltexprlem7  10993  reclem2pr  10999  reclem3pr  11000  reclem4pr  11001  supsrlem  11062  dissnref  23575  dissnlocfin  23576  txbas  23614  xkoccn  23666  xkoptsub  23701  xkoco1cn  23704  xkoco2cn  23705  xkoinjcn  23734  mbfi1fseqlem4  25767  avril1  30621  rnmposs  32835  bnj1436  35094  bnj916  35188  bnj983  35206  bnj1083  35233  bnj1245  35269  bnj1311  35279  bnj1371  35284  bnj1398  35289  tz9.1regs  35390  bj-elsngl  37413  bj-projun  37439  bj-projval  37441  f1omptsnlem  37790  icoreresf  37806  finxp0  37845  finxp1o  37846  finxpsuclem  37851  sdclem1  38202  csbcom2fi  38587  ralrnmo  38820  raldmqsmo  38822  rr-grothshortbi  44839  modelaxreplem3  45516