MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrnmptw Structured version   Visualization version   GIF version

Theorem ralrnmptw 6979
Description: A restricted quantifier over an image set. Version of ralrnmpt 6981 with a disjoint variable condition, which does not require ax-13 2373. (Contributed by Mario Carneiro, 20-Aug-2015.) (Revised by Gino Giotto, 26-Jan-2024.)
Hypotheses
Ref Expression
ralrnmptw.1 𝐹 = (𝑥𝐴𝐵)
ralrnmptw.2 (𝑦 = 𝐵 → (𝜓𝜒))
Assertion
Ref Expression
ralrnmptw (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝑦,𝐵   𝜒,𝑦   𝑦,𝐹   𝜓,𝑥
Allowed substitution hints:   𝜓(𝑦)   𝜒(𝑥)   𝐴(𝑦)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem ralrnmptw
Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralrnmptw.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
21fnmpt 6582 . . . 4 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
3 dfsbcq 3719 . . . . 5 (𝑤 = (𝐹𝑧) → ([𝑤 / 𝑦]𝜓[(𝐹𝑧) / 𝑦]𝜓))
43ralrn 6973 . . . 4 (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
52, 4syl 17 . . 3 (∀𝑥𝐴 𝐵𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
6 nfsbc1v 3737 . . . 4 𝑦[𝑤 / 𝑦]𝜓
7 nfv 1918 . . . 4 𝑤𝜓
8 sbceq2a 3729 . . . 4 (𝑤 = 𝑦 → ([𝑤 / 𝑦]𝜓𝜓))
96, 7, 8cbvralw 3374 . . 3 (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓)
10 nfmpt1 5183 . . . . . . 7 𝑥(𝑥𝐴𝐵)
111, 10nfcxfr 2906 . . . . . 6 𝑥𝐹
12 nfcv 2908 . . . . . 6 𝑥𝑧
1311, 12nffv 6793 . . . . 5 𝑥(𝐹𝑧)
14 nfv 1918 . . . . 5 𝑥𝜓
1513, 14nfsbcw 3739 . . . 4 𝑥[(𝐹𝑧) / 𝑦]𝜓
16 nfv 1918 . . . 4 𝑧[(𝐹𝑥) / 𝑦]𝜓
17 fveq2 6783 . . . . 5 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
1817sbceq1d 3722 . . . 4 (𝑧 = 𝑥 → ([(𝐹𝑧) / 𝑦]𝜓[(𝐹𝑥) / 𝑦]𝜓))
1915, 16, 18cbvralw 3374 . . 3 (∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓 ↔ ∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓)
205, 9, 193bitr3g 313 . 2 (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓))
211fvmpt2 6895 . . . . . 6 ((𝑥𝐴𝐵𝑉) → (𝐹𝑥) = 𝐵)
2221sbceq1d 3722 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓[𝐵 / 𝑦]𝜓))
23 ralrnmptw.2 . . . . . . 7 (𝑦 = 𝐵 → (𝜓𝜒))
2423sbcieg 3757 . . . . . 6 (𝐵𝑉 → ([𝐵 / 𝑦]𝜓𝜒))
2524adantl 482 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([𝐵 / 𝑦]𝜓𝜒))
2622, 25bitrd 278 . . . 4 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓𝜒))
2726ralimiaa 3087 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒))
28 ralbi 3090 . . 3 (∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒) → (∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∀𝑥𝐴 𝜒))
2927, 28syl 17 . 2 (∀𝑥𝐴 𝐵𝑉 → (∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∀𝑥𝐴 𝜒))
3020, 29bitrd 278 1 (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2107  wral 3065  [wsbc 3717  cmpt 5158  ran crn 5591   Fn wfn 6432  cfv 6437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-fv 6445
This theorem is referenced by:  rexrnmptw  6980  ac6num  10244  gsumwspan  18494  dfod2  19180  ordtbaslem  22348  ordtrest2lem  22363  cncmp  22552  comppfsc  22692  ptpjopn  22772  ordthmeolem  22961  tsmsfbas  23288  tsmsf1o  23305  prdsxmetlem  23530  prdsbl  23656  metdsf  24020  metdsge  24021  minveclem1  24597  minveclem3b  24601  minveclem6  24607  mbflimsup  24839  xrlimcnp  26127  minvecolem1  29245  minvecolem5  29252  minvecolem6  29253  ordtrest2NEWlem  31881  cvmsss2  33245  fin2so  35773  prdsbnd  35960  rrnequiv  36002  ralrnmpt3  42812
  Copyright terms: Public domain W3C validator