| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fvelimabd | Structured version Visualization version GIF version | ||
| Description: Deduction form of fvelimab 6894. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| Ref | Expression |
|---|---|
| fvelimabd.1 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
| fvelimabd.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| Ref | Expression |
|---|---|
| fvelimabd | ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvelimabd.1 | . 2 ⊢ (𝜑 → 𝐹 Fn 𝐴) | |
| 2 | fvelimabd.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | |
| 3 | fvelimab 6894 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) | |
| 4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑥 ∈ 𝐵 (𝐹‘𝑥) = 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1541 ∈ wcel 2111 ∃wrex 3056 ⊆ wss 3897 “ cima 5617 Fn wfn 6476 ‘cfv 6481 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pr 5368 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5090 df-opab 5152 df-id 5509 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-iota 6437 df-fun 6483 df-fn 6484 df-fv 6489 |
| This theorem is referenced by: unima 6897 resf1extb 7864 ghmqusnsglem1 19192 ghmquskerlem1 19195 lmhmima 20981 mdegldg 25998 ig1peu 26107 2ndimaxp 32628 fnpreimac 32653 fsuppcurry1 32707 fsuppcurry2 32708 swrdrn3 32936 esplyfv1 33590 esplyfv 33591 fnrelpredd 35102 bj-gabima 36984 extoimad 44256 upgrimpths 48008 |
| Copyright terms: Public domain | W3C validator |