Theorem eqabri 2902

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  eqabcri  2903  rabid  3432  csbcow  3861  csbco  3862  csbgfi  3866  csbnestgfw  4379  csbnestgf  4384  relopabi  5799  cnv0OLD  5861  funcnv3  6611  opabiota  6968  zfrep6OLD  7968  frrlem2  8309  frrlem3  8310  frrlem4  8311  frrlem8  8315  fprresex  8332  tfrlem4  8390  tfrlem8  8396  tfrlem9  8397  ixpn0  8962  sbthlem1  9110  dffi3  9427  setinds  9754  1idpr  11118  ltexprlem1  11125  ltexprlem2  11126  ltexprlem3  11127  ltexprlem4  11128  ltexprlem6  11130  ltexprlem7  11131  reclem2pr  11137  reclem3pr  11138  reclem4pr  11139  supsrlem  11200  dissnref  23853  dissnlocfin  23854  txbas  23892  xkoccn  23944  xkoptsub  23979  xkoco1cn  23982  xkoco2cn  23983  xkoinjcn  24012  mbfi1fseqlem4  26045  avril1  31070  rnmposs  33315  bnj1436  35516  bnj916  35610  bnj983  35628  bnj1083  35655  bnj1245  35691  bnj1311  35701  bnj1371  35706  bnj1398  35711  tz9.1regs  35859  bj-elsngl  37974  bj-projun  38000  bj-projval  38002  f1omptsnlem  38353  icoreresf  38369  finxp0  38408  finxp1o  38409  finxpsuclem  38414  dfproplem  38735  sdclem1  38771  csbcom2fi  39154  ralrnmo  39387  raldmqsmo  39389  rr-grothshortbi  45381  modelaxreplem3  46064