Theorem ralrnmpt 5935

Description: A restricted quantifier over an image set. (Contributed by Mario Carneiro, 20-Aug-2015.)

Hypotheses

Ref	Expression
ralrnmpt.1
ralrnmpt.2

Assertion

Ref	Expression
ralrnmpt

Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem ralrnmpt

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ralrnmpt.1	. . . . 5
2	1	fnmpt 5619	. . . 4
3		dfsbcq 3270	. . . . 5
4	3	ralrn 5929	. . . 4
5	2, 4	syl 16	. . 3
6		nfv 1674	. . . . 5
7		nfsbc1v 3288	. . . . 5
8		sbceq1a 3279	. . . . 5
9	6, 7, 8	cbvral 3023	. . . 4
10	9	bicomi 202	. . 3
11		nfmpt1 4463	. . . . . . 7
12	1, 11	nfcxfr 2608	. . . . . 6
13		nfcv 2610	. . . . . 6
14	12, 13	nffv 5780	. . . . 5
15		nfv 1674	. . . . 5
16	14, 15	nfsbc 3290	. . . 4
17		nfv 1674	. . . 4
18		fveq2 5773	. . . . 5
19		dfsbcq 3270	. . . . 5
20	18, 19	syl 16	. . . 4
21	16, 17, 20	cbvral 3023	. . 3
22	5, 10, 21	3bitr3g 287	. 2
23	1	fvmpt2 5864	. . . . . 6
24		dfsbcq 3270	. . . . . 6
25	23, 24	syl 16	. . . . 5
26		ralrnmpt.2	. . . . . . 7
27	26	sbcieg 3301	. . . . . 6
28	27	adantl 466	. . . . 5
29	25, 28	bitrd 253	. . . 4
30	29	ralimiaa 2869	. . 3
31		ralbi 2933	. . 3
32	30, 31	syl 16	. 2
33	22, 32	bitrd 253	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1370  e.wcel 1757  A.wral 2792  [.wsbc 3268  e.cmpt 4432  rancrn 4923  Fnwfn 5495  `cfv 5500

This theorem is referenced by:  rexrnmpt  5936  ac6num  8733  gsumwspan  15610  dfod2  16153  ordtbaslem  18892  ordtrest2lem  18907  cncmp  19095  ptpjopn  19285  ordthmeolem  19474  tsmsfbas  19798  tsmsf1o  19819  prdsxmetlem  20043  prdsbl  20166  metdsf  20524  metdsge  20525  minveclem1  21011  minveclem3b  21015  minveclem6  21021  mbflimsup  21244  xrlimcnp  22462  minvecolem1  24394  minvecolem5  24401  minvecolem6  24402  ordtrest2NEWlem  26470  cvmsss2  27281  fin2so  28538  comppfsc  28701  prdsbnd  28814  rrnequiv  28856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4495  ax-nul 4503  ax-pow 4552  ax-pr 4613

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-rab 2801  df-v 3054  df-sbc 3269  df-csb 3371  df-dif 3413  df-un 3415  df-in 3417  df-ss 3424  df-nul 3720  df-if 3874  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4174  df-br 4375  df-opab 4433  df-mpt 4434  df-id 4718  df-xp 4928  df-rel 4929  df-cnv 4930  df-co 4931  df-dm 4932  df-rn 4933  df-res 4934  df-ima 4935  df-iota 5463  df-fun 5502  df-fn 5503  df-fv 5508