Theorem eqabri 2883

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

Syntax hints:   ↔ wb 206   = wceq 1537  ⊤wtru 1538   ∈ wcel 2106  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814

This theorem is referenced by:  eqabcri  2884  rabid  3455  csbcow  3923  csbco  3924  csbgfi  3929  csbnestgfw  4428  csbnestgf  4433  ssrelOLD  5796  relopabi  5835  cnv0  6163  funcnv3  6638  opabiota  6991  zfrep6  7978  frrlem2  8311  frrlem3  8312  frrlem4  8313  frrlem8  8317  fprresex  8334  wfrlem2OLD  8348  wfrlem3OLD  8349  wfrlem4OLD  8351  wfrdmclOLD  8356  tfrlem4  8418  tfrlem8  8423  tfrlem9  8424  ixpn0  8969  sbthlem1  9122  dffi3  9469  1idpr  11067  ltexprlem1  11074  ltexprlem2  11075  ltexprlem3  11076  ltexprlem4  11077  ltexprlem6  11079  ltexprlem7  11080  reclem2pr  11086  reclem3pr  11087  reclem4pr  11088  supsrlem  11149  dissnref  23552  dissnlocfin  23553  txbas  23591  xkoccn  23643  xkoptsub  23678  xkoco1cn  23681  xkoco2cn  23682  xkoinjcn  23711  mbfi1fseqlem4  25768  avril1  30492  rnmposs  32691  bnj1436  34832  bnj916  34926  bnj983  34944  bnj1083  34971  bnj1245  35007  bnj1311  35017  bnj1371  35022  bnj1398  35027  setinds  35760  bj-elsngl  36951  bj-projun  36977  bj-projval  36979  f1omptsnlem  37319  icoreresf  37335  finxp0  37374  finxp1o  37375  finxpsuclem  37380  sdclem1  37730  csbcom2fi  38115  rr-grothshortbi  44299  modelaxreplem3  44945  upwordisword  46835  tworepnotupword  46840