| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fnerel 36339 | . . . . 5
⊢ Rel
Fne | 
| 2 | 1 | brrelex1i 5741 | . . . 4
⊢ (𝐴Fne𝐵 → 𝐴 ∈ V) | 
| 3 | 2 | anim1i 615 | . . 3
⊢ ((𝐴Fne𝐵 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) | 
| 4 | 3 | ancoms 458 | . 2
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴Fne𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) | 
| 5 |  | simpr 484 | . . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) | 
| 6 |  | isfne.1 | . . . . 5
⊢ 𝑋 = ∪
𝐴 | 
| 7 |  | isfne.2 | . . . . 5
⊢ 𝑌 = ∪
𝐵 | 
| 8 | 5, 6, 7 | 3eqtr3g 2800 | . . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → ∪ 𝐴 = ∪
𝐵) | 
| 9 |  | simpr 484 | . . . . . . 7
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐴 =
∪ 𝐵) | 
| 10 |  | uniexg 7760 | . . . . . . . 8
⊢ (𝐵 ∈ 𝐶 → ∪ 𝐵 ∈ V) | 
| 11 | 10 | adantr 480 | . . . . . . 7
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐵
∈ V) | 
| 12 | 9, 11 | eqeltrd 2841 | . . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐴
∈ V) | 
| 13 |  | uniexb 7784 | . . . . . 6
⊢ (𝐴 ∈ V ↔ ∪ 𝐴
∈ V) | 
| 14 | 12, 13 | sylibr 234 | . . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → 𝐴 ∈ V) | 
| 15 |  | simpl 482 | . . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → 𝐵 ∈ 𝐶) | 
| 16 | 14, 15 | jca 511 | . . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) | 
| 17 | 8, 16 | syldan 591 | . . 3
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) | 
| 18 | 17 | adantrr 717 | . 2
⊢ ((𝐵 ∈ 𝐶 ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) | 
| 19 |  | unieq 4918 | . . . . . 6
⊢ (𝑟 = 𝐴 → ∪ 𝑟 = ∪
𝐴) | 
| 20 | 19, 6 | eqtr4di 2795 | . . . . 5
⊢ (𝑟 = 𝐴 → ∪ 𝑟 = 𝑋) | 
| 21 | 20 | eqeq1d 2739 | . . . 4
⊢ (𝑟 = 𝐴 → (∪ 𝑟 = ∪
𝑠 ↔ 𝑋 = ∪ 𝑠)) | 
| 22 |  | raleq 3323 | . . . 4
⊢ (𝑟 = 𝐴 → (∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥))) | 
| 23 | 21, 22 | anbi12d 632 | . . 3
⊢ (𝑟 = 𝐴 → ((∪ 𝑟 = ∪
𝑠 ∧ ∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)) ↔ (𝑋 = ∪ 𝑠 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)))) | 
| 24 |  | unieq 4918 | . . . . . 6
⊢ (𝑠 = 𝐵 → ∪ 𝑠 = ∪
𝐵) | 
| 25 | 24, 7 | eqtr4di 2795 | . . . . 5
⊢ (𝑠 = 𝐵 → ∪ 𝑠 = 𝑌) | 
| 26 | 25 | eqeq2d 2748 | . . . 4
⊢ (𝑠 = 𝐵 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = 𝑌)) | 
| 27 |  | ineq1 4213 | . . . . . . 7
⊢ (𝑠 = 𝐵 → (𝑠 ∩ 𝒫 𝑥) = (𝐵 ∩ 𝒫 𝑥)) | 
| 28 | 27 | unieqd 4920 | . . . . . 6
⊢ (𝑠 = 𝐵 → ∪ (𝑠 ∩ 𝒫 𝑥) = ∪
(𝐵 ∩ 𝒫 𝑥)) | 
| 29 | 28 | sseq2d 4016 | . . . . 5
⊢ (𝑠 = 𝐵 → (𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) | 
| 30 | 29 | ralbidv 3178 | . . . 4
⊢ (𝑠 = 𝐵 → (∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) | 
| 31 | 26, 30 | anbi12d 632 | . . 3
⊢ (𝑠 = 𝐵 → ((𝑋 = ∪ 𝑠 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) | 
| 32 |  | df-fne 36338 | . . 3
⊢ Fne =
{〈𝑟, 𝑠〉 ∣ (∪ 𝑟 =
∪ 𝑠 ∧ ∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥))} | 
| 33 | 23, 31, 32 | brabg 5544 | . 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝐶) → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) | 
| 34 | 4, 18, 33 | pm5.21nd 802 | 1
⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) |