Theorem eqabri 2884

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

Syntax hints:   ↔ wb 206   = wceq 1539  ⊤wtru 1540   ∈ wcel 2107  {cab 2713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815

This theorem is referenced by:  eqabcri  2885  rabid  3457  csbcow  3913  csbco  3914  csbgfi  3918  csbnestgfw  4421  csbnestgf  4426  ssrelOLD  5792  relopabi  5831  cnv0  6159  funcnv3  6635  opabiota  6990  zfrep6  7980  frrlem2  8313  frrlem3  8314  frrlem4  8315  frrlem8  8319  fprresex  8336  wfrlem2OLD  8350  wfrlem3OLD  8351  wfrlem4OLD  8353  wfrdmclOLD  8358  tfrlem4  8420  tfrlem8  8425  tfrlem9  8426  ixpn0  8971  sbthlem1  9124  dffi3  9472  1idpr  11070  ltexprlem1  11077  ltexprlem2  11078  ltexprlem3  11079  ltexprlem4  11080  ltexprlem6  11082  ltexprlem7  11083  reclem2pr  11089  reclem3pr  11090  reclem4pr  11091  supsrlem  11152  dissnref  23537  dissnlocfin  23538  txbas  23576  xkoccn  23628  xkoptsub  23663  xkoco1cn  23666  xkoco2cn  23667  xkoinjcn  23696  mbfi1fseqlem4  25754  avril1  30483  rnmposs  32685  bnj1436  34854  bnj916  34948  bnj983  34966  bnj1083  34993  bnj1245  35029  bnj1311  35039  bnj1371  35044  bnj1398  35049  setinds  35780  bj-elsngl  36970  bj-projun  36996  bj-projval  36998  f1omptsnlem  37338  icoreresf  37354  finxp0  37393  finxp1o  37394  finxpsuclem  37399  sdclem1  37751  csbcom2fi  38136  rr-grothshortbi  44327  modelaxreplem3  45002  upwordisword  46901  tworepnotupword  46906