Theorem abeq2i 2764

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 2763	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↔ 𝜑))
4	3	trud 1533	1 ⊢ (𝑥 ∈ 𝐴 ↔ 𝜑)

Syntax hints:   ↔ wb 196   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030  {cab 2637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647

This theorem is referenced by:  abeq1i  2765  rabid  3145  vex  3234  csbco  3576  csbnestgf  4029  ssrel  5241  relopabi  5278  cnv0  5570  funcnv3  5997  opabiota  6300  zfrep6  7176  wfrlem2  7460  wfrlem3  7461  wfrlem4  7463  wfrdmcl  7468  tfrlem4  7520  tfrlem8  7525  tfrlem9  7526  ixpn0  7982  mapsnen  8076  sbthlem1  8111  dffi3  8378  1idpr  9889  ltexprlem1  9896  ltexprlem2  9897  ltexprlem3  9898  ltexprlem4  9899  ltexprlem6  9901  ltexprlem7  9902  reclem2pr  9908  reclem3pr  9909  reclem4pr  9910  supsrlem  9970  dissnref  21379  dissnlocfin  21380  txbas  21418  xkoccn  21470  xkoptsub  21505  xkoco1cn  21508  xkoco2cn  21509  xkoinjcn  21538  mbfi1fseqlem4  23530  avril1  27449  rnmpt2ss  29601  bnj1436  31036  bnj916  31129  bnj983  31147  bnj1083  31172  bnj1245  31208  bnj1311  31218  bnj1371  31223  bnj1398  31228  setinds  31807  frrlem2  31906  frrlem3  31907  frrlem4  31908  frrlem5e  31913  frrlem11  31917  bj-ififc  32691  bj-elsngl  33081  bj-projun  33107  bj-projval  33109  f1omptsnlem  33313  icoreresf  33330  finxp0  33358  finxp1o  33359  finxpsuclem  33364  sdclem1  33669  csbcom2fi  34064  csbgfi  34065