ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexrnmpt GIF version

Theorem rexrnmpt 5362
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
rexrnmpt (∀𝑥𝐴 𝐵𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥𝐴 𝜒))
Distinct variable groups:   𝑥,𝐴   𝑦,𝐵   𝜒,𝑦   𝑦,𝐹   𝜓,𝑥
Allowed substitution hints:   𝜓(𝑦)   𝜒(𝑥)   𝐴(𝑦)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥,𝑦)

Proof of Theorem rexrnmpt
Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ralrnmpt.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
21fnmpt 5076 . . . 4 (∀𝑥𝐴 𝐵𝑉𝐹 Fn 𝐴)
3 dfsbcq 2826 . . . . 5 (𝑤 = (𝐹𝑧) → ([𝑤 / 𝑦]𝜓[(𝐹𝑧) / 𝑦]𝜓))
43rexrn 5356 . . . 4 (𝐹 Fn 𝐴 → (∃𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∃𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
52, 4syl 14 . . 3 (∀𝑥𝐴 𝐵𝑉 → (∃𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∃𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓))
6 nfv 1462 . . . . 5 𝑤𝜓
7 nfsbc1v 2842 . . . . 5 𝑦[𝑤 / 𝑦]𝜓
8 sbceq1a 2833 . . . . 5 (𝑦 = 𝑤 → (𝜓[𝑤 / 𝑦]𝜓))
96, 7, 8cbvrex 2579 . . . 4 (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓)
109bicomi 130 . . 3 (∃𝑤 ∈ ran 𝐹[𝑤 / 𝑦]𝜓 ↔ ∃𝑦 ∈ ran 𝐹𝜓)
11 nfmpt1 3891 . . . . . . 7 𝑥(𝑥𝐴𝐵)
121, 11nfcxfr 2220 . . . . . 6 𝑥𝐹
13 nfcv 2223 . . . . . 6 𝑥𝑧
1412, 13nffv 5236 . . . . 5 𝑥(𝐹𝑧)
15 nfv 1462 . . . . 5 𝑥𝜓
1614, 15nfsbc 2844 . . . 4 𝑥[(𝐹𝑧) / 𝑦]𝜓
17 nfv 1462 . . . 4 𝑧[(𝐹𝑥) / 𝑦]𝜓
18 fveq2 5229 . . . . 5 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
1918sbceq1d 2829 . . . 4 (𝑧 = 𝑥 → ([(𝐹𝑧) / 𝑦]𝜓[(𝐹𝑥) / 𝑦]𝜓))
2016, 17, 19cbvrex 2579 . . 3 (∃𝑧𝐴 [(𝐹𝑧) / 𝑦]𝜓 ↔ ∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓)
215, 10, 203bitr3g 220 . 2 (∀𝑥𝐴 𝐵𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓))
221fvmpt2 5306 . . . . . 6 ((𝑥𝐴𝐵𝑉) → (𝐹𝑥) = 𝐵)
2322sbceq1d 2829 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓[𝐵 / 𝑦]𝜓))
24 ralrnmpt.2 . . . . . . 7 (𝑦 = 𝐵 → (𝜓𝜒))
2524sbcieg 2855 . . . . . 6 (𝐵𝑉 → ([𝐵 / 𝑦]𝜓𝜒))
2625adantl 271 . . . . 5 ((𝑥𝐴𝐵𝑉) → ([𝐵 / 𝑦]𝜓𝜒))
2723, 26bitrd 186 . . . 4 ((𝑥𝐴𝐵𝑉) → ([(𝐹𝑥) / 𝑦]𝜓𝜒))
2827ralimiaa 2430 . . 3 (∀𝑥𝐴 𝐵𝑉 → ∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒))
29 pm5.32 441 . . . . . 6 ((𝑥𝐴 → ([(𝐹𝑥) / 𝑦]𝜓𝜒)) ↔ ((𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ (𝑥𝐴𝜒)))
3029albii 1400 . . . . 5 (∀𝑥(𝑥𝐴 → ([(𝐹𝑥) / 𝑦]𝜓𝜒)) ↔ ∀𝑥((𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ (𝑥𝐴𝜒)))
31 exbi 1536 . . . . 5 (∀𝑥((𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ (𝑥𝐴𝜒)) → (∃𝑥(𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ ∃𝑥(𝑥𝐴𝜒)))
3230, 31sylbi 119 . . . 4 (∀𝑥(𝑥𝐴 → ([(𝐹𝑥) / 𝑦]𝜓𝜒)) → (∃𝑥(𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ ∃𝑥(𝑥𝐴𝜒)))
33 df-ral 2358 . . . 4 (∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒) ↔ ∀𝑥(𝑥𝐴 → ([(𝐹𝑥) / 𝑦]𝜓𝜒)))
34 df-rex 2359 . . . . 5 (∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∃𝑥(𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓))
35 df-rex 2359 . . . . 5 (∃𝑥𝐴 𝜒 ↔ ∃𝑥(𝑥𝐴𝜒))
3634, 35bibi12i 227 . . . 4 ((∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∃𝑥𝐴 𝜒) ↔ (∃𝑥(𝑥𝐴[(𝐹𝑥) / 𝑦]𝜓) ↔ ∃𝑥(𝑥𝐴𝜒)))
3732, 33, 363imtr4i 199 . . 3 (∀𝑥𝐴 ([(𝐹𝑥) / 𝑦]𝜓𝜒) → (∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∃𝑥𝐴 𝜒))
3828, 37syl 14 . 2 (∀𝑥𝐴 𝐵𝑉 → (∃𝑥𝐴 [(𝐹𝑥) / 𝑦]𝜓 ↔ ∃𝑥𝐴 𝜒))
3921, 38bitrd 186 1 (∀𝑥𝐴 𝐵𝑉 → (∃𝑦 ∈ ran 𝐹𝜓 ↔ ∃𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wal 1283   = wceq 1285  wex 1422  wcel 1434  wral 2353  wrex 2354  [wsbc 2824  cmpt 3859  ran crn 4392   Fn wfn 4947  cfv 4952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2612  df-sbc 2825  df-csb 2918  df-un 2986  df-in 2988  df-ss 2995  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-opab 3860  df-mpt 3861  df-id 4076  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-iota 4917  df-fun 4954  df-fn 4955  df-fv 4960
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator