| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elxp2 5709 | . . . . . 6
⊢ (𝑝 ∈ (𝐴 × 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉) | 
| 2 |  | nfcv 2905 | . . . . . . . . 9
⊢
Ⅎ𝑥Pred(𝑅, (𝐴 × 𝐵), 𝑝) | 
| 3 |  | nfsbc1v 3808 | . . . . . . . . 9
⊢
Ⅎ𝑥[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 | 
| 4 | 2, 3 | nfralw 3311 | . . . . . . . 8
⊢
Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 | 
| 5 |  | nfsbc1v 3808 | . . . . . . . 8
⊢
Ⅎ𝑥[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 | 
| 6 | 4, 5 | nfim 1896 | . . . . . . 7
⊢
Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) | 
| 7 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 | 
| 8 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑦Pred(𝑅, (𝐴 × 𝐵), 𝑝) | 
| 9 |  | nfcv 2905 | . . . . . . . . . . 11
⊢
Ⅎ𝑦(1st ‘𝑞) | 
| 10 |  | nfsbc1v 3808 | . . . . . . . . . . 11
⊢
Ⅎ𝑦[(2nd ‘𝑞) / 𝑦]𝜑 | 
| 11 | 9, 10 | nfsbcw 3810 | . . . . . . . . . 10
⊢
Ⅎ𝑦[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 | 
| 12 | 8, 11 | nfralw 3311 | . . . . . . . . 9
⊢
Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 | 
| 13 |  | nfcv 2905 | . . . . . . . . . 10
⊢
Ⅎ𝑦(1st ‘𝑝) | 
| 14 |  | nfsbc1v 3808 | . . . . . . . . . 10
⊢
Ⅎ𝑦[(2nd ‘𝑝) / 𝑦]𝜑 | 
| 15 | 13, 14 | nfsbcw 3810 | . . . . . . . . 9
⊢
Ⅎ𝑦[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 | 
| 16 | 12, 15 | nfim 1896 | . . . . . . . 8
⊢
Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) | 
| 17 |  | frpoins3xpg.2 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) | 
| 18 | 17 | sbcbidv 3845 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → ([(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(2nd ‘𝑞) / 𝑦]𝜓)) | 
| 19 | 18 | cbvsbcvw 3822 | . . . . . . . . . . . . . 14
⊢
([(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑦]𝜓) | 
| 20 |  | frpoins3xpg.3 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) | 
| 21 | 20 | cbvsbcvw 3822 | . . . . . . . . . . . . . . 15
⊢
([(2nd ‘𝑞) / 𝑦]𝜓 ↔ [(2nd ‘𝑞) / 𝑤]𝜒) | 
| 22 | 21 | sbcbii 3846 | . . . . . . . . . . . . . 14
⊢
([(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑦]𝜓 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) | 
| 23 | 19, 22 | bitri 275 | . . . . . . . . . . . . 13
⊢
([(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) | 
| 24 | 23 | ralbii 3093 | . . . . . . . . . . . 12
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒) | 
| 25 |  | impexp 450 | . . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒))) | 
| 26 |  | elin 3967 | . . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) | 
| 27 |  | predss 6329 | . . . . . . . . . . . . . . . . . . 19
⊢
Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ⊆ (𝐴 × 𝐵) | 
| 28 |  | sseqin2 4223 | . . . . . . . . . . . . . . . . . . 19
⊢
(Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ⊆ (𝐴 × 𝐵) ↔ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 29 | 27, 28 | mpbi 230 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) | 
| 30 | 29 | eleq2i 2833 | . . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 31 | 26, 30 | bitr3i 277 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 32 | 31 | imbi1i 349 | . . . . . . . . . . . . . . 15
⊢ (((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) | 
| 33 | 25, 32 | bitr3i 277 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) ↔ (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) | 
| 34 | 33 | albii 1819 | . . . . . . . . . . . . 13
⊢
(∀𝑞(𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) | 
| 35 |  | df-ral 3062 | . . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑞(𝑞 ∈ (𝐴 × 𝐵) → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒))) | 
| 36 |  | df-ral 3062 | . . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) | 
| 37 | 34, 35, 36 | 3bitr4ri 304 | . . . . . . . . . . . 12
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 ↔ ∀𝑞 ∈ (𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒)) | 
| 38 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) | 
| 39 |  | nfsbc1v 3808 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑧[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 | 
| 40 | 38, 39 | nfim 1896 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑧(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) | 
| 41 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤 𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) | 
| 42 |  | nfcv 2905 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤(1st ‘𝑞) | 
| 43 |  | nfsbc1v 3808 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤[(2nd ‘𝑞) / 𝑤]𝜒 | 
| 44 | 42, 43 | nfsbcw 3810 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑤[(1st ‘𝑞) / 𝑧][(2nd ‘𝑞) / 𝑤]𝜒 | 
| 45 | 41, 44 | nfim 1896 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑤(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) | 
| 46 |  | nfv 1914 | . . . . . . . . . . . . . 14
⊢
Ⅎ𝑞(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) | 
| 47 |  | eleq1 2829 | . . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑧, 𝑤〉 → (𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) | 
| 48 |  | sbcopeq1a 8074 | . . . . . . . . . . . . . . 15
⊢ (𝑞 = 〈𝑧, 𝑤〉 → ([(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒 ↔ 𝜒)) | 
| 49 | 47, 48 | imbi12d 344 | . . . . . . . . . . . . . 14
⊢ (𝑞 = 〈𝑧, 𝑤〉 → ((𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) | 
| 50 | 40, 45, 46, 49 | ralxpf 5857 | . . . . . . . . . . . . 13
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐵 (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 51 |  | r2al 3195 | . . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐵 (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) ↔ ∀𝑧∀𝑤((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) | 
| 52 |  | impexp 450 | . . . . . . . . . . . . . . . 16
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ (〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) | 
| 53 |  | opelxp 5721 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵)) | 
| 54 | 53 | imbi1i 349 | . . . . . . . . . . . . . . . 16
⊢
((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) | 
| 55 | 52, 54 | bitri 275 | . . . . . . . . . . . . . . 15
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒))) | 
| 56 |  | elin 3967 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ (〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉))) | 
| 57 | 29 | eleq2i 2833 | . . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, 𝑤〉 ∈ ((𝐴 × 𝐵) ∩ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 58 | 56, 57 | bitr3i 277 | . . . . . . . . . . . . . . . 16
⊢
((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) ↔ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 59 | 58 | imbi1i 349 | . . . . . . . . . . . . . . 15
⊢
(((〈𝑧, 𝑤〉 ∈ (𝐴 × 𝐵) ∧ 〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) → 𝜒) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 60 | 55, 59 | bitr3i 277 | . . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 61 | 60 | 2albii 1820 | . . . . . . . . . . . . 13
⊢
(∀𝑧∀𝑤((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → (〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 62 | 50, 51, 61 | 3bitri 297 | . . . . . . . . . . . 12
⊢
(∀𝑞 ∈
(𝐴 × 𝐵)(𝑞 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → [(1st
‘𝑞) / 𝑧][(2nd
‘𝑞) / 𝑤]𝜒) ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 63 | 24, 37, 62 | 3bitri 297 | . . . . . . . . . . 11
⊢
(∀𝑞 ∈
Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒)) | 
| 64 |  | frpoins3xpg.1 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧∀𝑤(〈𝑧, 𝑤〉 ∈ Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉) → 𝜒) → 𝜑)) | 
| 65 | 63, 64 | biimtrid 242 | . . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → 𝜑)) | 
| 66 |  | predeq3 6325 | . . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → Pred(𝑅, (𝐴 × 𝐵), 𝑝) = Pred(𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)) | 
| 67 | 66 | raleqdv 3326 | . . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑)) | 
| 68 |  | sbcopeq1a 8074 | . . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ([(1st
‘𝑝) / 𝑥][(2nd
‘𝑝) / 𝑦]𝜑 ↔ 𝜑)) | 
| 69 | 67, 68 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → ((∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 〈𝑥, 𝑦〉)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → 𝜑))) | 
| 70 | 65, 69 | syl5ibrcom 247 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑))) | 
| 71 | 70 | ex 412 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)))) | 
| 72 | 7, 16, 71 | rexlimd 3266 | . . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑))) | 
| 73 | 6, 72 | rexlimi 3259 | . . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝑝 = 〈𝑥, 𝑦〉 → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)) | 
| 74 | 1, 73 | sylbi 217 | . . . . 5
⊢ (𝑝 ∈ (𝐴 × 𝐵) → (∀𝑞 ∈ Pred (𝑅, (𝐴 × 𝐵), 𝑝)[(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑 → [(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑)) | 
| 75 |  | fveq2 6906 | . . . . . 6
⊢ (𝑝 = 𝑞 → (1st ‘𝑝) = (1st ‘𝑞)) | 
| 76 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞)) | 
| 77 | 76 | sbceq1d 3793 | . . . . . 6
⊢ (𝑝 = 𝑞 → ([(2nd ‘𝑝) / 𝑦]𝜑 ↔ [(2nd ‘𝑞) / 𝑦]𝜑)) | 
| 78 | 75, 77 | sbceqbid 3795 | . . . . 5
⊢ (𝑝 = 𝑞 → ([(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑 ↔ [(1st ‘𝑞) / 𝑥][(2nd ‘𝑞) / 𝑦]𝜑)) | 
| 79 | 74, 78 | frpoins2g 6366 | . . . 4
⊢ ((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) → ∀𝑝 ∈ (𝐴 × 𝐵)[(1st ‘𝑝) / 𝑥][(2nd ‘𝑝) / 𝑦]𝜑) | 
| 80 |  | ralxpes 8161 | . . . 4
⊢
(∀𝑝 ∈
(𝐴 × 𝐵)[(1st
‘𝑝) / 𝑥][(2nd
‘𝑝) / 𝑦]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | 
| 81 | 79, 80 | sylib 218 | . . 3
⊢ ((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) | 
| 82 |  | frpoins3xpg.4 | . . . 4
⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜃)) | 
| 83 |  | frpoins3xpg.5 | . . . 4
⊢ (𝑦 = 𝑌 → (𝜃 ↔ 𝜏)) | 
| 84 | 82, 83 | rspc2va 3634 | . . 3
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑) → 𝜏) | 
| 85 | 81, 84 | sylan2 593 | . 2
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) ∧ (𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵))) → 𝜏) | 
| 86 | 85 | ancoms 458 | 1
⊢ (((𝑅 Fr (𝐴 × 𝐵) ∧ 𝑅 Po (𝐴 × 𝐵) ∧ 𝑅 Se (𝐴 × 𝐵)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) → 𝜏) |