Theorem eqabri 2906

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  eqabcri  2907  rabid  3436  csbcow  3866  csbco  3867  csbgfi  3871  csbnestgfw  4383  csbnestgf  4388  relopabiOLD  5807  cnv0OLD  5870  funcnv3  6635  opabiota  6993  rnmposs  7581  zfrep6OLD  7994  frrlem2  8336  frrlem3  8337  frrlem4  8338  frrlem8  8342  fprresex  8359  tfrlem4  8417  tfrlem8  8423  tfrlem9  8424  ixpn0  8989  sbthlem1  9137  dffi3  9453  setinds  9780  1idpr  11144  ltexprlem1  11151  ltexprlem2  11152  ltexprlem3  11153  ltexprlem4  11154  ltexprlem6  11156  ltexprlem7  11157  reclem2pr  11163  reclem3pr  11164  reclem4pr  11165  supsrlem  11226  dissnref  23880  dissnlocfin  23881  txbas  23919  xkoccn  23971  xkoptsub  24006  xkoco1cn  24009  xkoco2cn  24010  xkoinjcn  24039  mbfi1fseqlem4  26072  avril1  31097  bnj1436  35552  bnj916  35646  bnj983  35664  bnj1083  35691  bnj1245  35727  bnj1311  35737  bnj1371  35742  bnj1398  35747  tz9.1regs  35915  bj-elsngl  38072  bj-projun  38098  bj-projval  38100  f1omptsnlem  38464  icoreresf  38480  finxp0  38519  finxp1o  38520  finxpsuclem  38525  dfproplem  38846  sdclem1  38880  csbcom2fi  39263  ralrnmo  39496  raldmqsmo  39498  rr-grothshortbi  45490  modelaxreplem3  46176