Theorem nfel 2262

Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfnfc.1	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfel	⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Proof of Theorem nfel

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-clel 2109	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝐵))
2		nfcv 2253	. . . . 5 ⊢ Ⅎ𝑥𝑧
3		nfnfc.1	. . . . 5 ⊢ Ⅎ𝑥𝐴
4	2, 3	nfeq 2261	. . . 4 ⊢ Ⅎ𝑥 𝑧 = 𝐴
5		nfeq.2	. . . . 5 ⊢ Ⅎ𝑥𝐵
6	5	nfcri 2247	. . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐵
7	4, 6	nfan 1525	. . 3 ⊢ Ⅎ𝑥(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝐵)
8	7	nfex 1597	. 2 ⊢ Ⅎ𝑥∃𝑧(𝑧 = 𝐴 ∧ 𝑧 ∈ 𝐵)
9	1, 8	nfxfr 1431	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:   ∧ wa 103   = wceq 1312  Ⅎwnf 1417  ∃wex 1449   ∈ wcel 1461  Ⅎwnfc 2240

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-cleq 2106  df-clel 2109  df-nfc 2242

This theorem is referenced by:  nfel1  2264  nfel2  2266  nfnel  2382  elabgf  2794  elrabf  2805  sbcel12g  2982  nfdisjv  3882  rabxfrd  4348  ffnfvf  5531  mptelixpg  6580  elabgft1  12668  elabgf2  12670  bj-rspgt  12676