Theorem eqabri 2876

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

Syntax hints:   ↔ wb 205   = wceq 1540  ⊤wtru 1541   ∈ wcel 2105  {cab 2708

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809

This theorem is referenced by:  eqabcri  2877  rabid  3451  csbcow  3908  csbco  3909  csbgfi  3914  csbnestgfw  4419  csbnestgf  4424  ssrelOLD  5783  relopabi  5822  cnv0  6140  funcnv3  6618  opabiota  6974  zfrep6  7945  frrlem2  8278  frrlem3  8279  frrlem4  8280  frrlem8  8284  fprresex  8301  wfrlem2OLD  8315  wfrlem3OLD  8316  wfrlem4OLD  8318  wfrdmclOLD  8323  tfrlem4  8385  tfrlem8  8390  tfrlem9  8391  ixpn0  8930  sbthlem1  9089  dffi3  9432  1idpr  11030  ltexprlem1  11037  ltexprlem2  11038  ltexprlem3  11039  ltexprlem4  11040  ltexprlem6  11042  ltexprlem7  11043  reclem2pr  11049  reclem3pr  11050  reclem4pr  11051  supsrlem  11112  dissnref  23353  dissnlocfin  23354  txbas  23392  xkoccn  23444  xkoptsub  23479  xkoco1cn  23482  xkoco2cn  23483  xkoinjcn  23512  mbfi1fseqlem4  25569  avril1  30151  rnmposs  32334  bnj1436  34316  bnj916  34410  bnj983  34428  bnj1083  34455  bnj1245  34491  bnj1311  34501  bnj1371  34506  bnj1398  34511  setinds  35222  bj-elsngl  36316  bj-projun  36342  bj-projval  36344  f1omptsnlem  36684  icoreresf  36700  finxp0  36739  finxp1o  36740  finxpsuclem  36745  sdclem1  37078  csbcom2fi  37463  rr-grothshortbi  43528  upwordisword  46057  tworepnotupword  46062