| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > inopab | Structured version Visualization version GIF version | ||
| Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.) |
| Ref | Expression |
|---|---|
| inopab | ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relopabv 5770 | . . 3 ⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | |
| 2 | relin1 5761 | . . 3 ⊢ (Rel {〈𝑥, 𝑦〉 ∣ 𝜑} → Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
| 3 | 1, 2 | ax-mp 5 | . 2 ⊢ Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) |
| 4 | relopabv 5770 | . 2 ⊢ Rel {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} | |
| 5 | sban 2085 | . . . 4 ⊢ ([𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)) | |
| 6 | sban 2085 | . . . . 5 ⊢ ([𝑤 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓)) | |
| 7 | 6 | sbbii 2081 | . . . 4 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓)) |
| 8 | vopelopabsb 5477 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | |
| 9 | vopelopabsb 5477 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) | |
| 10 | 8, 9 | anbi12i 628 | . . . 4 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)) |
| 11 | 5, 7, 10 | 3bitr4ri 304 | . . 3 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓)) |
| 12 | elin 3917 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
| 13 | vopelopabsb 5477 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓)) | |
| 14 | 11, 12, 13 | 3bitr4i 303 | . 2 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)}) |
| 15 | 3, 4, 14 | eqrelriiv 5739 | 1 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1541 [wsb 2067 ∈ wcel 2113 ∩ cin 3900 〈cop 4586 {copab 5160 Rel wrel 5629 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-opab 5161 df-xp 5630 df-rel 5631 |
| This theorem is referenced by: inxpOLD 5781 resopab 5993 fndmin 6990 cnvoprab 8004 epinid0 9508 cnvepnep 9517 wemapwe 9606 dfiso2 17696 frgpuplem 19701 pjfval2 21664 ltbwe 21999 opsrtoslem1 22010 lgsquadlem3 27349 disjecxrn 38597 br1cosscnvxrn 38737 1cosscnvxrn 38738 dnwech 43290 fgraphopab 43445 |
| Copyright terms: Public domain | W3C validator |