Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrnmpt Unicode version

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.
StepHypRef Expression
1 ralrnmpt.1 . . . . 5
21fnmpt 5619 . . . 4
3 dfsbcq 3270 . . . . 5
43ralrn 5929 . . . 4
52, 4syl 16 . . 3
6 nfv 1674 . . . . 5
7 nfsbc1v 3288 . . . . 5
8 sbceq1a 3279 . . . . 5
96, 7, 8cbvral 3023 . . . 4
109bicomi 202 . . 3
11 nfmpt1 4463 . . . . . . 7
121, 11nfcxfr 2608 . . . . . 6
13 nfcv 2610 . . . . . 6
1412, 13nffv 5780 . . . . 5
15 nfv 1674 . . . . 5
1614, 15nfsbc 3290 . . . 4
17 nfv 1674 . . . 4
18 fveq2 5773 . . . . 5
19 dfsbcq 3270 . . . . 5
2018, 19syl 16 . . . 4
2116, 17, 20cbvral 3023 . . 3
225, 10, 213bitr3g 287 . 2
231fvmpt2 5864 . . . . . 6
24 dfsbcq 3270 . . . . . 6
2523, 24syl 16 . . . . 5
26 ralrnmpt.2 . . . . . . 7
2726sbcieg 3301 . . . . . 6
2827adantl 466 . . . . 5
2925, 28bitrd 253 . . . 4
3029ralimiaa 2869 . . 3
31 ralbi 2933 . . 3
3230, 31syl 16 . 2
3322, 32bitrd 253 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator