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 1843 | . 2 ⊢ (𝜑 → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) |
3 | relssdv.1 | . . 3 ⊢ (𝜑 → Rel 𝐴) | |
4 | ssrel 5130 | . . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) | |
5 | 3, 4 | syl 17 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵))) |
6 | 2, 5 | mpbird 246 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 ∈ wcel 1977 ⊆ wss 3540 〈cop 4131 Rel wrel 5043 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-in 3547 df-ss 3554 df-opab 4644 df-xp 5044 df-rel 5045 |
This theorem is referenced by: relssres 5357 poirr2 5439 sofld 5500 relssdmrn 5573 funcres2 16381 wunfunc 16382 fthres2 16415 pospo 16796 joindmss 16830 meetdmss 16844 clatl 16939 subrgdvds 18617 opsrtoslem2 19306 txcls 21217 txdis1cn 21248 txkgen 21265 qustgplem 21734 metustid 22169 metustexhalf 22171 ovoliunlem1 23077 dvres2 23482 cvmlift2lem12 30550 dib2dim 35550 dih2dimbALTN 35552 dihmeetlem1N 35597 dihglblem5apreN 35598 dihmeetlem13N 35626 dihjatcclem4 35728 |
Copyright terms: Public domain | W3C validator |