Theorem relssi 4630

Description: Inference from subclass principle for relations. (Contributed by NM, 31-Mar-1998.)

Hypotheses

Ref	Expression
relssi.1	⊢ Rel 𝐴
relssi.2	⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)

Assertion

Ref	Expression
relssi	⊢ 𝐴 ⊆ 𝐵

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem relssi

Step	Hyp	Ref	Expression
1		relssi.1	. . 3 ⊢ Rel 𝐴
2		ssrel 4627	. . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
3	1, 2	ax-mp 5	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
4		relssi.2	. . 3 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)
5	4	ax-gen 1425	. 2 ⊢ ∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)
6	3, 5	mpgbir 1429	1 ⊢ 𝐴 ⊆ 𝐵

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329   ∈ wcel 1480   ⊆ wss 3071  ⟨cop 3530  Rel wrel 4544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-opab 3990  df-xp 4545  df-rel 4546

This theorem is referenced by:  resiexg  4864  dftpos4  6160  enssdom  6656  idssen  6671  txuni2  12425