Theorem relssdv 5786

Description: Deduction from subclass principle for relations. (Contributed by NM, 11-Sep-2004.)

Hypotheses

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

Assertion

Ref	Expression
relssdv	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

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

Proof of Theorem relssdv

Step	Hyp	Ref	Expression
1		relssdv.2	. . 3 ⊢ (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
2	1	alrimivv 1931	. 2 ⊢ (𝜑 → ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵))
3		relssdv.1	. . 3 ⊢ (𝜑 → Rel 𝐴)
4		ssrel 5780	. . 3 ⊢ (Rel 𝐴 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ ∀𝑥∀𝑦(⟨𝑥, 𝑦⟩ ∈ 𝐴 → ⟨𝑥, 𝑦⟩ ∈ 𝐵)))
6	2, 5	mpbird 256	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2106   ⊆ wss 3947  ⟨cop 4633  Rel wrel 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  relssres  6020  poirr2  6122  sofld  6183  relssdmrn  6264  relssdmrnOLD  6265  funcres2  17844  wunfunc  17845  wunfuncOLD  17846  fthres2  17879  pospo  18294  joindmss  18328  meetdmss  18342  clatl  18457  subrgdvds  20369  opsrtoslem2  21608  txcls  23099  txdis1cn  23130  txkgen  23147  qustgplem  23616  metustid  24054  metustexhalf  24056  ovoliunlem1  25010  dvres2  25420  cvmlift2lem12  34293  dib2dim  40102  dih2dimbALTN  40104  dihmeetlem1N  40149  dihglblem5apreN  40150  dihmeetlem13N  40178  dihjatcclem4  40280