Theorem eqabri 2872

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  eqabcri  2873  rabid  3430  csbcow  3880  csbco  3881  csbgfi  3885  csbnestgfw  4388  csbnestgf  4393  ssrelOLD  5749  relopabi  5788  cnv0  6116  funcnv3  6589  opabiota  6946  zfrep6  7936  frrlem2  8269  frrlem3  8270  frrlem4  8271  frrlem8  8275  fprresex  8292  tfrlem4  8350  tfrlem8  8355  tfrlem9  8356  ixpn0  8906  sbthlem1  9057  dffi3  9389  1idpr  10989  ltexprlem1  10996  ltexprlem2  10997  ltexprlem3  10998  ltexprlem4  10999  ltexprlem6  11001  ltexprlem7  11002  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010  supsrlem  11071  dissnref  23422  dissnlocfin  23423  txbas  23461  xkoccn  23513  xkoptsub  23548  xkoco1cn  23551  xkoco2cn  23552  xkoinjcn  23581  mbfi1fseqlem4  25626  avril1  30399  rnmposs  32605  bnj1436  34836  bnj916  34930  bnj983  34948  bnj1083  34975  bnj1245  35011  bnj1311  35021  bnj1371  35026  bnj1398  35031  setinds  35773  bj-elsngl  36963  bj-projun  36989  bj-projval  36991  f1omptsnlem  37331  icoreresf  37347  finxp0  37386  finxp1o  37387  finxpsuclem  37392  sdclem1  37744  csbcom2fi  38129  rr-grothshortbi  44299  modelaxreplem3  44977  upwordisword  46886  tworepnotupword  46891