Theorem eqabri 2878

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

Syntax hints:   ↔ wb 206   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eqabcri  2879  rabid  3410  csbcow  3852  csbco  3853  csbgfi  3857  csbnestgfw  4362  csbnestgf  4367  relopabi  5778  cnv0OLD  6104  funcnv3  6568  opabiota  6922  zfrep6OLD  7908  frrlem2  8237  frrlem3  8238  frrlem4  8239  frrlem8  8243  fprresex  8260  tfrlem4  8318  tfrlem8  8323  tfrlem9  8324  ixpn0  8878  sbthlem1  9025  dffi3  9344  setinds  9670  1idpr  10952  ltexprlem1  10959  ltexprlem2  10960  ltexprlem3  10961  ltexprlem4  10962  ltexprlem6  10964  ltexprlem7  10965  reclem2pr  10971  reclem3pr  10972  reclem4pr  10973  supsrlem  11034  dissnref  23493  dissnlocfin  23494  txbas  23532  xkoccn  23584  xkoptsub  23619  xkoco1cn  23622  xkoco2cn  23623  xkoinjcn  23652  mbfi1fseqlem4  25685  avril1  30533  rnmposs  32746  bnj1436  34981  bnj916  35075  bnj983  35093  bnj1083  35120  bnj1245  35156  bnj1311  35166  bnj1371  35171  bnj1398  35176  tz9.1regs  35278  bj-elsngl  37275  bj-projun  37301  bj-projval  37303  f1omptsnlem  37652  icoreresf  37668  finxp0  37707  finxp1o  37708  finxpsuclem  37713  sdclem1  38064  csbcom2fi  38449  ralrnmo  38682  raldmqsmo  38684  rr-grothshortbi  44730  modelaxreplem3  45407