Theorem eqabri 2908

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⊤wtru 1571   ∈ wcel 2146  {cab 2744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841

This theorem is used by:  eqabcri  2909  rabid  3440  csbcow  3871  csbco  3872  csbgfi  3876  csbnestgfw  4390  csbnestgf  4395  relopabi  5814  cnv0OLD  5875  funcnv3  6613  opabiota  6970  zfrep6OLD  7961  frrlem2  8293  frrlem3  8294  frrlem4  8295  frrlem8  8299  fprresex  8316  tfrlem4  8374  tfrlem8  8380  tfrlem9  8381  ixpn0  8937  sbthlem1  9085  dffi3  9401  setinds  9728  1idpr  11032  ltexprlem1  11039  ltexprlem2  11040  ltexprlem3  11041  ltexprlem4  11042  ltexprlem6  11044  ltexprlem7  11045  reclem2pr  11051  reclem3pr  11052  reclem4pr  11053  supsrlem  11114  dissnref  23722  dissnlocfin  23723  txbas  23761  xkoccn  23813  xkoptsub  23848  xkoco1cn  23851  xkoco2cn  23852  xkoinjcn  23881  mbfi1fseqlem4  25914  avril1  30851  rnmposs  33055  bnj1436  35259  bnj916  35353  bnj983  35371  bnj1083  35398  bnj1245  35434  bnj1311  35444  bnj1371  35449  bnj1398  35454  tz9.1regs  35571  bj-elsngl  37645  bj-projun  37671  bj-projval  37673  f1omptsnlem  38023  icoreresf  38039  finxp0  38078  finxp1o  38079  finxpsuclem  38084  sdclem1  38435  csbcom2fi  38818  ralrnmo  39051  raldmqsmo  39053  rr-grothshortbi  45054  modelaxreplem3  45730