![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > relssdv | Structured version Visualization version GIF version |
Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.) |
Ref | Expression |
---|---|
relssdv.1 | ⊢ (𝜑 → Rel 𝐴) |
relssdv.2 | ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) |
Ref | Expression |
---|---|
relssdv | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relssdv.2 | . . 3 ⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | |
2 | 1 | alrimivv 1926 | . 2 ⊢ (𝜑 → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | relssdv.1 | . . 3 ⊢ (𝜑 → Rel 𝐴) | |
4 | ssrel 5795 | . . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) | |
5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) |
6 | 2, 5 | mpbird 257 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 ∈ wcel 2106 ⊆ wss 3963 〈cop 4637 Rel wrel 5694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-ss 3980 df-opab 5211 df-xp 5695 df-rel 5696 |
This theorem is referenced by: relssres 6042 poirr2 6147 sofld 6209 relssdmrn 6290 relssdmrnOLD 6291 funcres2 17949 wunfunc 17952 wunfuncOLD 17953 fthres2 17986 pospo 18403 joindmss 18437 meetdmss 18451 clatl 18566 subrgdvds 20603 opsrtoslem2 22098 txcls 23628 txdis1cn 23659 txkgen 23676 qustgplem 24145 metustid 24583 metustexhalf 24585 ovoliunlem1 25551 dvres2 25962 cvmlift2lem12 35299 dib2dim 41226 dih2dimbALTN 41228 dihmeetlem1N 41273 dihglblem5apreN 41274 dihmeetlem13N 41302 dihjatcclem4 41404 |
Copyright terms: Public domain | W3C validator |