Metamath Proof Explorer

Theorem undmrnresiss

Description: Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg . (Contributed by RP, 26-Sep-2020)

Ref Expression
Assertion undmrnresiss ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐵 𝑥 ∧ 𝑦 𝐵 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 resundi ⊢ ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) = ( ( I ↾ dom 𝐴 ) ∪ ( I ↾ ran 𝐴 ) )
2 1 sseq1i ⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐵 ↔ ( ( I ↾ dom 𝐴 ) ∪ ( I ↾ ran 𝐴 ) ) ⊆ 𝐵 )
3 unss ⊢ ( ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴 ) ⊆ 𝐵 ) ↔ ( ( I ↾ dom 𝐴 ) ∪ ( I ↾ ran 𝐴 ) ) ⊆ 𝐵 )
4 relres ⊢ Rel ( I ↾ dom 𝐴 )
5 ssrel ⊢ ( Rel ( I ↾ dom 𝐴 ) → ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 ) ) )
6 4 5 ax-mp ⊢ ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 ) )
7 vex ⊢ 𝑥 ∈ V
8 7 eldm ⊢ ( 𝑥 ∈ dom 𝐴 ↔ ∃ 𝑦 𝑥 𝐴 𝑦 )
9 df-br ⊢ ( 𝑥 I 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ I )
10 vex ⊢ 𝑧 ∈ V
11 10 ideq ⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
12 9 11 bitr3i ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ I ↔ 𝑥 = 𝑧 )
13 8 12 anbi12ci ⊢ ( ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ I ) ↔ ( 𝑥 = 𝑧 ∧ ∃ 𝑦 𝑥 𝐴 𝑦 ) )
14 10 opelresi ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) ↔ ( 𝑥 ∈ dom 𝐴 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ I ) )
15 19.42v ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) ↔ ( 𝑥 = 𝑧 ∧ ∃ 𝑦 𝑥 𝐴 𝑦 ) )
16 13 14 15 3bitr4i ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) ↔ ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) )
17 df-br ⊢ ( 𝑥 𝐵 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 )
18 17 bicomi ⊢ ( ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 ↔ 𝑥 𝐵 𝑧 )
19 16 18 imbi12i ⊢ ( ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
20 19 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ⟨ 𝑥 , 𝑧 ⟩ ∈ ( I ↾ dom 𝐴 ) → ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑧 ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
21 19.23v ⊢ ( ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
22 21 bicomi ⊢ ( ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
23 22 2albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
24 alcom ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) )
25 ancomst ⊢ ( ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 = 𝑧 ) → 𝑥 𝐵 𝑧 ) )
26 impexp ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑥 = 𝑧 ) → 𝑥 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) )
27 25 26 bitri ⊢ ( ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) )
28 27 albii ⊢ ( ∀ 𝑧 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) )
29 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) ↔ ( 𝑥 𝐴 𝑦 → ∀ 𝑧 ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) )
30 equcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
31 30 imbi1i ⊢ ( ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ↔ ( 𝑧 = 𝑥 → 𝑥 𝐵 𝑧 ) )
32 31 albii ⊢ ( ∀ 𝑧 ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 = 𝑥 → 𝑥 𝐵 𝑧 ) )
33 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 𝐵 𝑧 ↔ 𝑥 𝐵 𝑥 ) )
34 33 equsalvw ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑥 → 𝑥 𝐵 𝑧 ) ↔ 𝑥 𝐵 𝑥 )
35 32 34 bitri ⊢ ( ∀ 𝑧 ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ↔ 𝑥 𝐵 𝑥 )
36 35 imbi2i ⊢ ( ( 𝑥 𝐴 𝑦 → ∀ 𝑧 ( 𝑥 = 𝑧 → 𝑥 𝐵 𝑧 ) ) ↔ ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
37 28 29 36 3bitri ⊢ ( ∀ 𝑧 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
38 37 albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
39 24 38 bitri ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
40 39 albii ⊢ ( ∀ 𝑥 ∀ 𝑧 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
41 23 40 bitri ⊢ ( ∀ 𝑥 ∀ 𝑧 ( ∃ 𝑦 ( 𝑥 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑥 𝐵 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
42 6 20 41 3bitri ⊢ ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) )
43 relres ⊢ Rel ( I ↾ ran 𝐴 )
44 ssrel ⊢ ( Rel ( I ↾ ran 𝐴 ) → ( ( I ↾ ran 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑦 ∀ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ) ) )
45 43 44 ax-mp ⊢ ( ( I ↾ ran 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑦 ∀ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ) )
46 vex ⊢ 𝑦 ∈ V
47 46 elrn ⊢ ( 𝑦 ∈ ran 𝐴 ↔ ∃ 𝑥 𝑥 𝐴 𝑦 )
48 df-br ⊢ ( 𝑦 I 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ I )
49 10 ideq ⊢ ( 𝑦 I 𝑧 ↔ 𝑦 = 𝑧 )
50 48 49 bitr3i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ I ↔ 𝑦 = 𝑧 )
51 47 50 anbi12ci ⊢ ( ( 𝑦 ∈ ran 𝐴 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ I ) ↔ ( 𝑦 = 𝑧 ∧ ∃ 𝑥 𝑥 𝐴 𝑦 ) )
52 10 opelresi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) ↔ ( 𝑦 ∈ ran 𝐴 ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ I ) )
53 19.42v ⊢ ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) ↔ ( 𝑦 = 𝑧 ∧ ∃ 𝑥 𝑥 𝐴 𝑦 ) )
54 51 52 53 3bitr4i ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) ↔ ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) )
55 df-br ⊢ ( 𝑦 𝐵 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
56 55 bicomi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ↔ 𝑦 𝐵 𝑧 )
57 54 56 imbi12i ⊢ ( ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
58 57 2albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ↾ ran 𝐴 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
59 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
60 59 bicomi ⊢ ( ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑥 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
61 60 2albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
62 alrot3 ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) )
63 ancomst ⊢ ( ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 = 𝑧 ) → 𝑦 𝐵 𝑧 ) )
64 impexp ⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 = 𝑧 ) → 𝑦 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) )
65 63 64 bitri ⊢ ( ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) )
66 65 albii ⊢ ( ∀ 𝑧 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) )
67 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) ↔ ( 𝑥 𝐴 𝑦 → ∀ 𝑧 ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) )
68 equcom ⊢ ( 𝑦 = 𝑧 ↔ 𝑧 = 𝑦 )
69 68 imbi1i ⊢ ( ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ↔ ( 𝑧 = 𝑦 → 𝑦 𝐵 𝑧 ) )
70 69 albii ⊢ ( ∀ 𝑧 ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 = 𝑦 → 𝑦 𝐵 𝑧 ) )
71 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑦 𝐵 𝑧 ↔ 𝑦 𝐵 𝑦 ) )
72 71 equsalvw ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 → 𝑦 𝐵 𝑧 ) ↔ 𝑦 𝐵 𝑦 )
73 70 72 bitri ⊢ ( ∀ 𝑧 ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ↔ 𝑦 𝐵 𝑦 )
74 73 imbi2i ⊢ ( ( 𝑥 𝐴 𝑦 → ∀ 𝑧 ( 𝑦 = 𝑧 → 𝑦 𝐵 𝑧 ) ) ↔ ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) )
75 66 67 74 3bitri ⊢ ( ∀ 𝑧 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) )
76 75 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) )
77 61 62 76 3bitr2i ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ∃ 𝑥 ( 𝑦 = 𝑧 ∧ 𝑥 𝐴 𝑦 ) → 𝑦 𝐵 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) )
78 45 58 77 3bitri ⊢ ( ( I ↾ ran 𝐴 ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) )
79 42 78 anbi12i ⊢ ( ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴 ) ⊆ 𝐵 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) ) )
80 19.26-2 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) ∧ ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) ) )
81 pm4.76 ⊢ ( ( ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) ∧ ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) ) ↔ ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐵 𝑥 ∧ 𝑦 𝐵 𝑦 ) ) )
82 81 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 𝐴 𝑦 → 𝑥 𝐵 𝑥 ) ∧ ( 𝑥 𝐴 𝑦 → 𝑦 𝐵 𝑦 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐵 𝑥 ∧ 𝑦 𝐵 𝑦 ) ) )
83 79 80 82 3bitr2i ⊢ ( ( ( I ↾ dom 𝐴 ) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴 ) ⊆ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐵 𝑥 ∧ 𝑦 𝐵 𝑦 ) ) )
84 2 3 83 3bitr2i ⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐵 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐵 𝑥 ∧ 𝑦 𝐵 𝑦 ) ) )