Theorem abeq2i 2735

Description: Equality of a class variable and a class abstraction (inference rule). (Contributed by NM, 3-Apr-1996.) (Proof shortened by Wolf Lammen, 15-Nov-2019.)

Hypothesis

Ref	Expression
abeq2i.1	⊢ 𝐴 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
abeq2i	⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Proof of Theorem abeq2i

Step	Hyp	Ref	Expression
1		abeq2i.1	. . . 4 ⊢ 𝐴 = {𝑥 ∣ 𝜑}
2	1	a1i 11	. . 3 ⊢ (⊤ → 𝐴 = {𝑥 ∣ 𝜑})
3	2	abeq2d 2734	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	trud 1493	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 196   = wceq 1483  ⊤wtru 1484   ∈ wcel 1990  {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618

This theorem is referenced by:  abeq1i  2736  rabid  3116  vex  3203  csbco  3543  csbnestgf  3996  ssrel  5207  relopabi  5245  cnv0  5535  funcnv3  5959  opabiota  6261  zfrep6  7134  wfrlem2  7415  wfrlem3  7416  wfrlem4  7418  wfrdmcl  7423  tfrlem4  7475  tfrlem8  7480  tfrlem9  7481  ixpn0  7940  mapsnen  8035  sbthlem1  8070  dffi3  8337  1idpr  9851  ltexprlem1  9858  ltexprlem2  9859  ltexprlem3  9860  ltexprlem4  9861  ltexprlem6  9863  ltexprlem7  9864  reclem2pr  9870  reclem3pr  9871  reclem4pr  9872  supsrlem  9932  dissnref  21331  dissnlocfin  21332  txbas  21370  xkoccn  21422  xkoptsub  21457  xkoco1cn  21460  xkoco2cn  21461  xkoinjcn  21490  mbfi1fseqlem4  23485  avril1  27319  rnmpt2ss  29473  bnj1436  30910  bnj916  31003  bnj983  31021  bnj1083  31046  bnj1245  31082  bnj1311  31092  bnj1371  31097  bnj1398  31102  setinds  31683  frrlem2  31781  frrlem3  31782  frrlem4  31783  frrlem5e  31788  frrlem11  31792  bj-ififc  32566  bj-elsngl  32956  bj-projun  32982  bj-projval  32984  f1omptsnlem  33183  icoreresf  33200  finxp0  33228  finxp1o  33229  finxpsuclem  33234  sdclem1  33539  csbcom2fi  33934  csbgfi  33935