Theorem eqabri 2874

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

Syntax hints:   ↔ wb 206   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111  {cab 2709

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eqabcri  2875  rabid  3416  csbcow  3865  csbco  3866  csbgfi  3870  csbnestgfw  4372  csbnestgf  4377  relopabi  5762  cnv0  6087  funcnv3  6551  opabiota  6904  zfrep6  7887  frrlem2  8217  frrlem3  8218  frrlem4  8219  frrlem8  8223  fprresex  8240  tfrlem4  8298  tfrlem8  8303  tfrlem9  8304  ixpn0  8854  sbthlem1  9000  dffi3  9315  setinds  9639  1idpr  10920  ltexprlem1  10927  ltexprlem2  10928  ltexprlem3  10929  ltexprlem4  10930  ltexprlem6  10932  ltexprlem7  10933  reclem2pr  10939  reclem3pr  10940  reclem4pr  10941  supsrlem  11002  dissnref  23444  dissnlocfin  23445  txbas  23483  xkoccn  23535  xkoptsub  23570  xkoco1cn  23573  xkoco2cn  23574  xkoinjcn  23603  mbfi1fseqlem4  25647  avril1  30441  rnmposs  32654  bnj1436  34849  bnj916  34943  bnj983  34961  bnj1083  34988  bnj1245  35024  bnj1311  35034  bnj1371  35039  bnj1398  35044  tz9.1regs  35128  bj-elsngl  37008  bj-projun  37034  bj-projval  37036  f1omptsnlem  37376  icoreresf  37392  finxp0  37431  finxp1o  37432  finxpsuclem  37437  sdclem1  37789  csbcom2fi  38174  rr-grothshortbi  44342  modelaxreplem3  45019