| Step | Hyp | Ref
| Expression |
| 1 | | frege118.y |
. . . 4
⊢ 𝑌 ∈ 𝑉 |
| 2 | 1 | frege58c 43934 |
. . 3
⊢
(∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → [𝑌 / 𝑏](𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
| 3 | | sbcimg 3837 |
. . . . 5
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑏](𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) ↔ ([𝑌 / 𝑏]𝑏𝑅𝑋 → [𝑌 / 𝑏]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)))) |
| 4 | 1, 3 | ax-mp 5 |
. . . 4
⊢
([𝑌 / 𝑏](𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) ↔ ([𝑌 / 𝑏]𝑏𝑅𝑋 → [𝑌 / 𝑏]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋))) |
| 5 | | sbcbr1g 5200 |
. . . . . . 7
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑏]𝑏𝑅𝑋 ↔ ⦋𝑌 / 𝑏⦌𝑏𝑅𝑋)) |
| 6 | 1, 5 | ax-mp 5 |
. . . . . 6
⊢
([𝑌 / 𝑏]𝑏𝑅𝑋 ↔ ⦋𝑌 / 𝑏⦌𝑏𝑅𝑋) |
| 7 | | csbvarg 4434 |
. . . . . . . 8
⊢ (𝑌 ∈ 𝑉 → ⦋𝑌 / 𝑏⦌𝑏 = 𝑌) |
| 8 | 1, 7 | ax-mp 5 |
. . . . . . 7
⊢
⦋𝑌 /
𝑏⦌𝑏 = 𝑌 |
| 9 | 8 | breq1i 5150 |
. . . . . 6
⊢
(⦋𝑌 /
𝑏⦌𝑏𝑅𝑋 ↔ 𝑌𝑅𝑋) |
| 10 | 6, 9 | bitri 275 |
. . . . 5
⊢
([𝑌 / 𝑏]𝑏𝑅𝑋 ↔ 𝑌𝑅𝑋) |
| 11 | | sbcal 3849 |
. . . . . 6
⊢
([𝑌 / 𝑏]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ ∀𝑎[𝑌 / 𝑏](𝑏𝑅𝑎 → 𝑎 = 𝑋)) |
| 12 | | sbcimg 3837 |
. . . . . . . . 9
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑏](𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ ([𝑌 / 𝑏]𝑏𝑅𝑎 → [𝑌 / 𝑏]𝑎 = 𝑋))) |
| 13 | 1, 12 | ax-mp 5 |
. . . . . . . 8
⊢
([𝑌 / 𝑏](𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ ([𝑌 / 𝑏]𝑏𝑅𝑎 → [𝑌 / 𝑏]𝑎 = 𝑋)) |
| 14 | | sbcbr1g 5200 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑏]𝑏𝑅𝑎 ↔ ⦋𝑌 / 𝑏⦌𝑏𝑅𝑎)) |
| 15 | 1, 14 | ax-mp 5 |
. . . . . . . . . 10
⊢
([𝑌 / 𝑏]𝑏𝑅𝑎 ↔ ⦋𝑌 / 𝑏⦌𝑏𝑅𝑎) |
| 16 | 8 | breq1i 5150 |
. . . . . . . . . 10
⊢
(⦋𝑌 /
𝑏⦌𝑏𝑅𝑎 ↔ 𝑌𝑅𝑎) |
| 17 | 15, 16 | bitri 275 |
. . . . . . . . 9
⊢
([𝑌 / 𝑏]𝑏𝑅𝑎 ↔ 𝑌𝑅𝑎) |
| 18 | | sbcg 3863 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝑉 → ([𝑌 / 𝑏]𝑎 = 𝑋 ↔ 𝑎 = 𝑋)) |
| 19 | 1, 18 | ax-mp 5 |
. . . . . . . . 9
⊢
([𝑌 / 𝑏]𝑎 = 𝑋 ↔ 𝑎 = 𝑋) |
| 20 | 17, 19 | imbi12i 350 |
. . . . . . . 8
⊢
(([𝑌 / 𝑏]𝑏𝑅𝑎 → [𝑌 / 𝑏]𝑎 = 𝑋) ↔ (𝑌𝑅𝑎 → 𝑎 = 𝑋)) |
| 21 | 13, 20 | bitri 275 |
. . . . . . 7
⊢
([𝑌 / 𝑏](𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ (𝑌𝑅𝑎 → 𝑎 = 𝑋)) |
| 22 | 21 | albii 1819 |
. . . . . 6
⊢
(∀𝑎[𝑌 / 𝑏](𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)) |
| 23 | 11, 22 | bitri 275 |
. . . . 5
⊢
([𝑌 / 𝑏]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋) ↔ ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)) |
| 24 | 10, 23 | imbi12i 350 |
. . . 4
⊢
(([𝑌 / 𝑏]𝑏𝑅𝑋 → [𝑌 / 𝑏]∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) ↔ (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) |
| 25 | 4, 24 | bitri 275 |
. . 3
⊢
([𝑌 / 𝑏](𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) ↔ (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) |
| 26 | 2, 25 | sylib 218 |
. 2
⊢
(∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) |
| 27 | | frege116.x |
. . 3
⊢ 𝑋 ∈ 𝑈 |
| 28 | 27 | frege117 43993 |
. 2
⊢
((∀𝑏(𝑏𝑅𝑋 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑋)) → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) → (Fun ◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋)))) |
| 29 | 26, 28 | ax-mp 5 |
1
⊢ (Fun
◡◡𝑅 → (𝑌𝑅𝑋 → ∀𝑎(𝑌𝑅𝑎 → 𝑎 = 𝑋))) |