Theorem elab2g 2930

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)

Hypotheses

Ref	Expression
elab2g.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elab2g.2	⊢ 𝐵 = {𝑥 ∣ 𝜑}

Assertion

Ref	Expression
elab2g	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem elab2g

Step	Hyp	Ref	Expression
1		elab2g.2	. . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑}
2	1	eleq2i 2276	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
3		elab2g.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elabg 2929	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
5	2, 4	bitrid 192	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ∈ wcel 2180  {cab 2195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-v 2781

This theorem is referenced by:  elab2  2931  elab4g  2932  eldif  3186  elun  3325  elin  3367  elif  3594  elsng  3661  elprg  3666  eluni  3870  eliun  3948  eliin  3949  elopab  4325  elong  4441  opeliunxp  4751  elrn2g  4889  eldmg  4895  elrnmpt  4949  elrnmpt1  4951  elimag  5048  elrnmpog  6088  eloprabi  6312  tfrlem3ag  6425  tfr1onlem3ag  6453  tfrcllemsucaccv  6470  elqsg  6702  elixp2  6819  isomni  7271  ismkv  7288  iswomni  7300  isacnm  7353  1idprl  7745  1idpru  7746  recexprlemell  7777  recexprlemelu  7778  mertenslemub  12011  mertenslemi1  12012  mertenslem2  12013  4sqexercise1  12887  4sqexercise2  12888  4sqlemsdc  12889  ismgm  13356  istopg  14638  isbasisg  14683  2sqlem8  15767  2sqlem9  15768  isuhgrm  15836  isushgrm  15837  isupgren  15860  isumgren  15870  isuspgren  15920  isusgren  15921