| 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 5760 | . . 3 ⊢ Rel {〈𝑥, 𝑦〉 ∣ 𝜑} | |
| 2 | relin1 5751 | . . 3 ⊢ (Rel {〈𝑥, 𝑦〉 ∣ 𝜑} → Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
| 3 | 1, 2 | ax-mp 5 | . 2 ⊢ Rel ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) |
| 4 | relopabv 5760 | . 2 ⊢ Rel {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} | |
| 5 | sban 2083 | . . . 4 ⊢ ([𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)) | |
| 6 | sban 2083 | . . . . 5 ⊢ ([𝑤 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓)) | |
| 7 | 6 | sbbii 2079 | . . . 4 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑧 / 𝑥]([𝑤 / 𝑦]𝜑 ∧ [𝑤 / 𝑦]𝜓)) |
| 8 | vopelopabsb 5467 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | |
| 9 | vopelopabsb 5467 | . . . . 5 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓) | |
| 10 | 8, 9 | anbi12i 628 | . . . 4 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜓)) |
| 11 | 5, 7, 10 | 3bitr4ri 304 | . . 3 ⊢ ((〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓)) |
| 12 | elin 3913 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ∧ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜓})) | |
| 13 | vopelopabsb 5467 | . . 3 ⊢ (〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} ↔ [𝑧 / 𝑥][𝑤 / 𝑦](𝜑 ∧ 𝜓)) | |
| 14 | 11, 12, 13 | 3bitr4i 303 | . 2 ⊢ (〈𝑧, 𝑤〉 ∈ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) ↔ 〈𝑧, 𝑤〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)}) |
| 15 | 3, 4, 14 | eqrelriiv 5729 | 1 ⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ∩ {〈𝑥, 𝑦〉 ∣ 𝜓}) = {〈𝑥, 𝑦〉 ∣ (𝜑 ∧ 𝜓)} |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1541 [wsb 2067 ∈ wcel 2111 ∩ cin 3896 〈cop 4579 {copab 5151 Rel wrel 5619 |
| 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 2113 ax-9 2121 ax-10 2144 ax-12 2180 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pr 5368 |
| 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 2710 df-cleq 2723 df-clel 2806 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-opab 5152 df-xp 5620 df-rel 5621 |
| This theorem is referenced by: inxpOLD 5771 resopab 5982 fndmin 6978 cnvoprab 7992 epinid0 9489 cnvepnep 9498 wemapwe 9587 dfiso2 17679 frgpuplem 19684 pjfval2 21646 ltbwe 21979 opsrtoslem1 21990 lgsquadlem3 27320 disjecxrn 38435 br1cosscnvxrn 38575 1cosscnvxrn 38576 dnwech 43140 fgraphopab 43295 |
| Copyright terms: Public domain | W3C validator |