Theorem eqabri 2888

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eqabcri  2889  rabid  3465  csbcow  3936  csbco  3937  csbgfi  3942  csbnestgfw  4445  csbnestgf  4450  ssrelOLD  5807  relopabi  5846  cnv0  6172  funcnv3  6648  opabiota  7004  zfrep6  7995  frrlem2  8328  frrlem3  8329  frrlem4  8330  frrlem8  8334  fprresex  8351  wfrlem2OLD  8365  wfrlem3OLD  8366  wfrlem4OLD  8368  wfrdmclOLD  8373  tfrlem4  8435  tfrlem8  8440  tfrlem9  8441  ixpn0  8988  sbthlem1  9149  dffi3  9500  1idpr  11098  ltexprlem1  11105  ltexprlem2  11106  ltexprlem3  11107  ltexprlem4  11108  ltexprlem6  11110  ltexprlem7  11111  reclem2pr  11117  reclem3pr  11118  reclem4pr  11119  supsrlem  11180  dissnref  23557  dissnlocfin  23558  txbas  23596  xkoccn  23648  xkoptsub  23683  xkoco1cn  23686  xkoco2cn  23687  xkoinjcn  23716  mbfi1fseqlem4  25773  avril1  30495  rnmposs  32692  bnj1436  34815  bnj916  34909  bnj983  34927  bnj1083  34954  bnj1245  34990  bnj1311  35000  bnj1371  35005  bnj1398  35010  setinds  35742  bj-elsngl  36934  bj-projun  36960  bj-projval  36962  f1omptsnlem  37302  icoreresf  37318  finxp0  37357  finxp1o  37358  finxpsuclem  37363  sdclem1  37703  csbcom2fi  38088  rr-grothshortbi  44272  upwordisword  46800  tworepnotupword  46805