![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeliunxp2f | Structured version Visualization version GIF version |
Description: Membership in a union of Cartesian products, using bound-variable hypothesis for 𝐸 instead of distinct variable conditions as in opeliunxp2 5798. (Contributed by AV, 25-Oct-2020.) |
Ref | Expression |
---|---|
opeliunxp2f.f | ⊢ Ⅎ𝑥𝐸 |
opeliunxp2f.e | ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) |
Ref | Expression |
---|---|
opeliunxp2f | ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 5110 | . . 3 ⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) | |
2 | relxp 5655 | . . . . . 6 ⊢ Rel ({𝑥} × 𝐵) | |
3 | 2 | rgenw 3065 | . . . . 5 ⊢ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵) |
4 | reliun 5776 | . . . . 5 ⊢ (Rel ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵)) | |
5 | 3, 4 | mpbir 230 | . . . 4 ⊢ Rel ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
6 | 5 | brrelex1i 5692 | . . 3 ⊢ (𝐶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)𝐷 → 𝐶 ∈ V) |
7 | 1, 6 | sylbir 234 | . 2 ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝐶 ∈ V) |
8 | elex 3465 | . . 3 ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ V) | |
9 | 8 | adantr 482 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) → 𝐶 ∈ V) |
10 | nfiu1 4992 | . . . . 5 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) | |
11 | 10 | nfel2 2922 | . . . 4 ⊢ Ⅎ𝑥⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
12 | nfv 1918 | . . . . 5 ⊢ Ⅎ𝑥 𝐶 ∈ 𝐴 | |
13 | opeliunxp2f.f | . . . . . 6 ⊢ Ⅎ𝑥𝐸 | |
14 | 13 | nfel2 2922 | . . . . 5 ⊢ Ⅎ𝑥 𝐷 ∈ 𝐸 |
15 | 12, 14 | nfan 1903 | . . . 4 ⊢ Ⅎ𝑥(𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸) |
16 | 11, 15 | nfbi 1907 | . . 3 ⊢ Ⅎ𝑥(⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
17 | opeq1 4834 | . . . . 5 ⊢ (𝑥 = 𝐶 → ⟨𝑥, 𝐷⟩ = ⟨𝐶, 𝐷⟩) | |
18 | 17 | eleq1d 2819 | . . . 4 ⊢ (𝑥 = 𝐶 → (⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
19 | eleq1 2822 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | |
20 | opeliunxp2f.e | . . . . . 6 ⊢ (𝑥 = 𝐶 → 𝐵 = 𝐸) | |
21 | 20 | eleq2d 2820 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝐷 ∈ 𝐵 ↔ 𝐷 ∈ 𝐸)) |
22 | 19, 21 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝐶 → ((𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
23 | 18, 22 | bibi12d 346 | . . 3 ⊢ (𝑥 = 𝐶 → ((⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) ↔ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)))) |
24 | opeliunxp 5703 | . . 3 ⊢ (⟨𝑥, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) | |
25 | 16, 23, 24 | vtoclg1f 3526 | . 2 ⊢ (𝐶 ∈ V → (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸))) |
26 | 7, 9, 25 | pm5.21nii 380 | 1 ⊢ (⟨𝐶, 𝐷⟩ ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 Ⅎwnfc 2884 ∀wral 3061 Vcvv 3447 {csn 4590 ⟨cop 4596 ∪ ciun 4958 class class class wbr 5109 × cxp 5635 Rel wrel 5642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-iun 4960 df-br 5110 df-opab 5172 df-xp 5643 df-rel 5644 |
This theorem is referenced by: mpoxeldm 8146 fsumcom2 15667 fprodcom2 15875 iunsnima2 31591 |
Copyright terms: Public domain | W3C validator |