Theorem eqabri 2903

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

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

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 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  eqabcri  2904  rabid  3433  csbcow  3862  csbco  3863  csbgfi  3867  csbnestgfw  4380  csbnestgf  4385  relopabi  5800  cnv0OLD  5862  funcnv3  6602  opabiota  6959  zfrep6OLD  7956  frrlem2  8289  frrlem3  8290  frrlem4  8291  frrlem8  8295  fprresex  8312  tfrlem4  8370  tfrlem8  8376  tfrlem9  8377  ixpn0  8942  sbthlem1  9090  dffi3  9407  setinds  9734  1idpr  11095  ltexprlem1  11102  ltexprlem2  11103  ltexprlem3  11104  ltexprlem4  11105  ltexprlem6  11107  ltexprlem7  11108  reclem2pr  11114  reclem3pr  11115  reclem4pr  11116  supsrlem  11177  dissnref  23827  dissnlocfin  23828  txbas  23866  xkoccn  23918  xkoptsub  23953  xkoco1cn  23956  xkoco2cn  23957  xkoinjcn  23986  mbfi1fseqlem4  26019  avril1  31046  rnmposs  33249  bnj1436  35452  bnj916  35546  bnj983  35564  bnj1083  35591  bnj1245  35627  bnj1311  35637  bnj1371  35642  bnj1398  35647  tz9.1regs  35775  bj-elsngl  37851  bj-projun  37877  bj-projval  37879  f1omptsnlem  38227  icoreresf  38243  finxp0  38282  finxp1o  38283  finxpsuclem  38288  dfproplem  38609  sdclem1  38645  csbcom2fi  39028  ralrnmo  39261  raldmqsmo  39263  rr-grothshortbi  45246  modelaxreplem3  45922