Theorem ssrel 4351

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 2912	. . 3 ⊢ (A ⊆ B → (⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))
2	1	alrimivv 1733	. 2 ⊢ (A ⊆ B → ∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B))
3		eleq1 2078	. . . . . . . . . . 11 ⊢ (z = ⟨x, y⟩ → (z ∈ A ↔ ⟨x, y⟩ ∈ A))
4		eleq1 2078	. . . . . . . . . . 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 1321	. . . . . . . 8 ⊢ (∀x∀y(⟨x, y⟩ ∈ A → ⟨x, y⟩ ∈ B) → ∀x∀y(z = ⟨x, y⟩ → (z ∈ A → z ∈ B)))
8		19.23vv 1742	. . . . . . . 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 1737	. . . 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 4275	. . . . 5 ⊢ (Rel A ↔ A ⊆ (V × V))
14		dfss2 2907	. . . . 5 ⊢ (A ⊆ (V × V) ↔ ∀z(z ∈ A → z ∈ (V × V)))
15		elvv 4325	. . . . . . 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 1335	. . . . 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 2907	. . . 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 1224   = wceq 1226  ∃wex 1358   ∈ wcel 1370  Vcvv 2531   ⊆ wss 2890  ⟨cop 3349   × cxp 4266  Rel wrel 4273

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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-opab 3789  df-xp 4274  df-rel 4275

This theorem is referenced by:  eqrel  4352  relssi  4354  relssdv  4355  cotr  4629  cnvsym  4631  intasym  4632  intirr  4634  codir  4636  qfto  4637