| Step | Hyp | Ref
| Expression |
| 1 | | rabexg 5337 |
. 2
⊢ (𝐵 ∈ 𝑀 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V) |
| 2 | | ssrab2 4080 |
. . . 4
⊢ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 |
| 3 | 2 | a1i 11 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵) |
| 4 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑦 𝑥 ∈ 𝐴 |
| 5 | | nfre1 3285 |
. . . . 5
⊢
Ⅎ𝑦∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 |
| 6 | | sbceq2a 3800 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑)) |
| 7 | 6 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑) |
| 8 | 7 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑) |
| 9 | 8 | anim1ci 616 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)) |
| 10 | 9 | anasss 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)) |
| 11 | 10 | ancoms 458 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)) |
| 12 | | sbceq2a 3800 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑 ↔ 𝜑)) |
| 13 | 12 | sbcbidv 3845 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑤 / 𝑥]𝜑)) |
| 14 | 13 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)) |
| 15 | 14 | elrab 3692 |
. . . . . . . . 9
⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)) |
| 16 | 11, 15 | sylibr 234 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}) |
| 17 | | sbceq2a 3800 |
. . . . . . . . 9
⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑 ↔ 𝜑)) |
| 18 | 17 | rspcev 3622 |
. . . . . . . 8
⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑) |
| 19 | 16, 18 | sylancom 588 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑) |
| 20 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑣{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} |
| 21 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑦𝐴 |
| 22 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑤 |
| 23 | | nfsbc1v 3808 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦[𝑧 / 𝑦]𝜑 |
| 24 | 22, 23 | nfsbcw 3810 |
. . . . . . . . . 10
⊢
Ⅎ𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑 |
| 25 | 21, 24 | nfrexw 3313 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 |
| 26 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐵 |
| 27 | 25, 26 | nfrabw 3475 |
. . . . . . . 8
⊢
Ⅎ𝑦{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} |
| 28 | | nfsbc1v 3808 |
. . . . . . . 8
⊢
Ⅎ𝑦[𝑣 / 𝑦]𝜑 |
| 29 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑣𝜑 |
| 30 | 20, 27, 28, 29, 17 | cbvrexfw 3305 |
. . . . . . 7
⊢
(∃𝑣 ∈
{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑) |
| 31 | 19, 30 | sylib 218 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑) |
| 32 | 31 | exp31 419 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))) |
| 33 | 4, 5, 32 | rexlimd 3266 |
. . . 4
⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)) |
| 34 | 33 | ralimia 3080 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑) |
| 35 | | nfsbc1v 3808 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑤 / 𝑥]𝜑 |
| 36 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑤𝜑 |
| 37 | 35, 36, 6 | cbvrexw 3307 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑) |
| 38 | 14, 37 | bitrdi 287 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)) |
| 39 | 38 | elrab 3692 |
. . . . . 6
⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑)) |
| 40 | 39 | simprbi 496 |
. . . . 5
⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥 ∈ 𝐴 𝜑) |
| 41 | 40 | rgen 3063 |
. . . 4
⊢
∀𝑦 ∈
{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑 |
| 42 | 41 | a1i 11 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) |
| 43 | 3, 34, 42 | 3jca 1129 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) |
| 44 | | sseq1 4009 |
. . . . 5
⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐 ⊆ 𝐵 ↔ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)) |
| 45 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝐴 |
| 46 | | nfsbc1v 3808 |
. . . . . . . . 9
⊢
Ⅎ𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑 |
| 47 | 45, 46 | nfrexw 3313 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 |
| 48 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐵 |
| 49 | 47, 48 | nfrabw 3475 |
. . . . . . 7
⊢
Ⅎ𝑥{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} |
| 50 | 49 | nfeq2 2923 |
. . . . . 6
⊢
Ⅎ𝑥 𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} |
| 51 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦𝑐 |
| 52 | 51, 27 | rexeqf 3354 |
. . . . . 6
⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)) |
| 53 | 50, 52 | ralbid 3273 |
. . . . 5
⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)) |
| 54 | 51, 27 | raleqf 3353 |
. . . . 5
⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) |
| 55 | 44, 53, 54 | 3anbi123d 1438 |
. . . 4
⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))) |
| 56 | 55 | spcegv 3597 |
. . 3
⊢ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
| 57 | 56 | imp 406 |
. 2
⊢ (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |
| 58 | 1, 43, 57 | syl2an 596 |
1
⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |