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

Theorem ralrnmpt 7051
Description: A restricted quantifier over an image set. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker ralrnmptw 7049 when possible. (Contributed by Mario Carneiro, 20-Aug-2015.) (New usage is discouraged.)
Hypotheses
Ref Expression
ralrnmpt.1 𝐹 = (𝑥𝐴𝐵)
ralrnmpt.2 (𝑦 = 𝐵 → (𝜓𝜒))
Assertion
Ref Expression
ralrnmpt (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝑥,𝐴   𝑦,𝐵   𝜒,𝑦   𝑦,𝐹   𝜓,𝑥
Allowed substitution hints:   𝜓(𝑦)   𝜒(𝑥)   𝐴(𝑦)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem ralrnmpt
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralrnmpt.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
21fnmpt 6646 . . . 4 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
3 dfsbcq 3744 . . . . 5 (𝑤 = (𝐹𝑧) → ([𝑤 / 𝑦]𝜓[(𝐹𝑧) / 𝑦]𝜓))
43ralrn 7043 . . . 4 (𝐹 Fn 𝐴 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
52, 4syl 17 . . 3 (∀𝑥𝐴 𝐵𝑉 → (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
6 nfv 1917 . . . . 5 𝑤𝜓
7 nfsbc1v 3762 . . . . 5 𝑦[𝑤 / 𝑦]𝜓
8 sbceq1a 3753 . . . . 5 (𝑦 = 𝑤 → (𝜓[𝑤 / 𝑦]𝜓))
96, 7, 8cbvral 3333 . . . 4 (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓)
109bicomi 223 . . 3 (∀𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∀𝑦 ∈ ran 𝐹𝜓)
11 nfmpt1 5218 . . . . . . 7 𝑥(𝑥𝐴𝐵)
121, 11nfcxfr 2900 . . . . . 6 𝑥𝐹
13 nfcv 2902 . . . . . 6 𝑥𝑧
1412, 13nffv 6857 . . . . 5 𝑥(𝐹𝑧)
15 nfv 1917 . . . . 5 𝑥𝜓
1614, 15nfsbc 3767 . . . 4 𝑥[(𝐹𝑧) / 𝑦]𝜓
17 nfv 1917 . . . 4 𝑧[(𝐹𝑥) / 𝑦]𝜓
18 fveq2 6847 . . . . 5 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
1918sbceq1d 3747 . . . 4 (𝑧 = 𝑥 → ([(𝐹𝑧) / 𝑦]𝜓[(𝐹𝑥) / 𝑦]𝜓))
2016, 17, 19cbvral 3333 . . 3 (∀𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓 ↔ ∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓)
215, 10, 203bitr3g 312 . 2 (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓))
221fvmpt2 6964 . . . . . 6 ((𝑥𝐴𝐵𝑉) → (𝐹𝑥) = 𝐵)
2322sbceq1d 3747 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓[𝐵 / 𝑦]𝜓))
24 ralrnmpt.2 . . . . . . 7 (𝑦 = 𝐵 → (𝜓𝜒))
2524sbcieg 3782 . . . . . 6 (𝐵𝑉 → ([𝐵 / 𝑦]𝜓𝜒))
2625adantl 482 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([𝐵 / 𝑦]𝜓𝜒))
2723, 26bitrd 278 . . . 4 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓𝜒))
2827ralimiaa 3081 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒))
29 ralbi 3102 . . 3 (∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒) → (∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∀𝑥𝐴 𝜒))
3028, 29syl 17 . 2 (∀𝑥𝐴 𝐵𝑉 → (∀𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∀𝑥𝐴 𝜒))
3121, 30bitrd 278 1 (∀𝑥𝐴 𝐵𝑉 → (∀𝑦 ∈ ran 𝐹𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wral 3060  [wsbc 3742  cmpt 5193  ran crn 5639   Fn wfn 6496  cfv 6501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2370  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-fv 6509
This theorem is referenced by:  rexrnmpt  7052
  Copyright terms: Public domain W3C validator