Theorem ssrel 4371

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of [Monk1] p. 33. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
ssrel	⊢ (Rel A → (A ⊆ B ↔ ∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B)))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem ssrel

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 2933	. . 3 ⊢ (A ⊆ B → (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))
2	1	alrimivv 1752	. 2 ⊢ (A ⊆ B → ∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))
3		eleq1 2097	. . . . . . . . . . 11 ⊢ (z = ⟨x, y⟩ → (z ∈ A ↔ ⟨x, y⟩ ∈ A))
4		eleq1 2097	. . . . . . . . . . 11 ⊢ (z = ⟨x, y⟩ → (z ∈ B ↔ ⟨x, y⟩ ∈ B))
5	3, 4	imbi12d 223	. . . . . . . . . 10 ⊢ (z = ⟨x, y⟩ → ((z ∈ A → z ∈ B) ↔ (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B)))
6	5	biimprcd 149	. . . . . . . . 9 ⊢ ((⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → (z = ⟨x, y⟩ → (z ∈ A → z ∈ B)))
7	6	2alimi 1342	. . . . . . . 8 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → ∀x∀y(z = ⟨x, y⟩ → (z ∈ A → z ∈ B)))
8		19.23vv 1761	. . . . . . . 8 ⊢ (∀x∀y(z = ⟨x, y⟩ → (z ∈ A → z ∈ B)) ↔ (∃x∃y z = ⟨x, y⟩ → (z ∈ A → z ∈ B)))
9	7, 8	sylib 127	. . . . . . 7 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → (∃x∃y z = ⟨x, y⟩ → (z ∈ A → z ∈ B)))
10	9	com23 72	. . . . . 6 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → (z ∈ A → (∃x∃y z = ⟨x, y⟩ → z ∈ B)))
11	10	a2d 23	. . . . 5 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → ((z ∈ A → ∃x∃y z = ⟨x, y⟩) → (z ∈ A → z ∈ B)))
12	11	alimdv 1756	. . . 4 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → (∀z(z ∈ A → ∃x∃y z = ⟨x, y⟩) → ∀z(z ∈ A → z ∈ B)))
13		df-rel 4295	. . . . 5 ⊢ (Rel A ↔ A ⊆ (V × V))
14		dfss2 2928	. . . . 5 ⊢ (A ⊆ (V × V) ↔ ∀z(z ∈ A → z ∈ (V × V)))
15		elvv 4345	. . . . . . 7 ⊢ (z ∈ (V × V) ↔ ∃x∃y z = ⟨x, y⟩)
16	15	imbi2i 215	. . . . . 6 ⊢ ((z ∈ A → z ∈ (V × V)) ↔ (z ∈ A → ∃x∃y z = ⟨x, y⟩))
17	16	albii 1356	. . . . 5 ⊢ (∀z(z ∈ A → z ∈ (V × V)) ↔ ∀z(z ∈ A → ∃x∃y z = ⟨x, y⟩))
18	13, 14, 17	3bitri 195	. . . 4 ⊢ (Rel A ↔ ∀z(z ∈ A → ∃x∃y z = ⟨x, y⟩))
19		dfss2 2928	. . . 4 ⊢ (A ⊆ B ↔ ∀z(z ∈ A → z ∈ B))
20	12, 18, 19	3imtr4g 194	. . 3 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → (Rel A → A ⊆ B))
21	20	com12 27	. 2 ⊢ (Rel A → (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → A ⊆ B))
22	2, 21	impbid2 131	1 ⊢ (Rel A → (A ⊆ B ↔ ∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B)))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1240   = wceq 1242  ∃wex 1378   ∈ wcel 1390  Vcvv 2551   ⊆ wss 2911  ⟨cop 3370   × cxp 4286  Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294  df-rel 4295

This theorem is referenced by:  eqrel  4372  relssi  4374  relssdv  4375  cotr  4649  cnvsym  4651  intasym  4652  intirr  4654  codir  4656  qfto  4657