|   | 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 1927 | . 2 ⊢ (𝜑 → ∀𝑥∀𝑦(〈𝑥, 𝑦〉 ∈ 𝐴 → 〈𝑥, 𝑦〉 ∈ 𝐵)) | 
| 3 | relssdv.1 | . . 3 ⊢ (𝜑 → Rel 𝐴) | |
| 4 | ssrel 5791 | . . 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 1537 ∈ wcel 2107 ⊆ wss 3950 〈cop 4631 Rel wrel 5689 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-ss 3967 df-opab 5205 df-xp 5690 df-rel 5691 | 
| This theorem is referenced by: relssres 6039 poirr2 6143 sofld 6206 relssdmrn 6287 relssdmrnOLD 6288 funcres2 17944 wunfunc 17947 fthres2 17980 pospo 18391 joindmss 18425 meetdmss 18439 clatl 18554 subrgdvds 20587 opsrtoslem2 22081 txcls 23613 txdis1cn 23644 txkgen 23661 qustgplem 24130 metustid 24568 metustexhalf 24570 ovoliunlem1 25538 dvres2 25948 cvmlift2lem12 35320 dib2dim 41246 dih2dimbALTN 41248 dihmeetlem1N 41293 dihglblem5apreN 41294 dihmeetlem13N 41322 dihjatcclem4 41424 | 
| Copyright terms: Public domain | W3C validator |