Theorem elrabf 3255

Description: Membership in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable restrictions. (Contributed by NM, 21-Sep-2003.)

Hypotheses

Ref	Expression
elrabf.1
elrabf.2
elrabf.3
elrabf.4

Assertion

Ref	Expression
elrabf

Proof of Theorem elrabf

Step	Hyp	Ref	Expression
1		elex 3118	. 2
2		elex 3118	. . 3
3	2	adantr 465	. 2
4		df-rab 2816	. . . 4
5	4	eleq2i 2535	. . 3
6		elrabf.1	. . . 4
7		elrabf.2	. . . . . 6
8	6, 7	nfel 2632	. . . . 5
9		elrabf.3	. . . . 5
10	8, 9	nfan 1928	. . . 4
11		eleq1 2529	. . . . 5
12		elrabf.4	. . . . 5
13	11, 12	anbi12d 710	. . . 4
14	6, 10, 13	elabgf 3244	. . 3
15	5, 14	syl5bb 257	. 2
16	1, 3, 15	pm5.21nii 353	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  F/wnf 1616  e.wcel 1818  {cab 2442  F/_wnfc 2605  {crab 2811  cvv 3109

This theorem is referenced by:  elrab  3257  rabasiun  4334  rabxfrd  4673  onminsb  6634  nnawordex  7305  tskwe  8352  rabssnn0fi  12095  iundisj  21958  iundisjf  27448  iundisjfi  27601  sltval2  29416  nobndlem5  29456  rfcnpre3  31408  rfcnpre4  31409  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem34  31816  stoweidlem51  31833  stoweidlem52  31834  stoweidlem59  31841  fourierdlem20  31909  fourierdlem79  31968  bnj1388  34089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111