Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opelresi | Structured version Visualization version GIF version |
Description: Ordered pair membership in a restriction. Exercise 13 of [TakeutiZaring] p. 25. (Contributed by NM, 13-Nov-1995.) |
Ref | Expression |
---|---|
opelresi.1 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
opelresi | ⊢ (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelresi.1 | . 2 ⊢ 𝐶 ∈ V | |
2 | opelres 5875 | . 2 ⊢ (𝐶 ∈ V → (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∈ wcel 2112 Vcvv 3423 〈cop 4564 ↾ cres 5571 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pr 5339 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2717 df-cleq 2731 df-clel 2818 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-in 3890 df-nul 4255 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-opab 5133 df-xp 5575 df-res 5581 |
This theorem is referenced by: opres 5879 dmres 5891 relssres 5910 iss 5921 restidsing 5940 asymref 5999 ssrnres 6059 cnvresima 6111 ressn 6166 funssres 6445 fcnvres 6618 fvn0ssdmfun 6917 relexpindlem 14659 dprd2dlem1 19461 dprd2da 19462 hausdiag 22574 hauseqlcld 22575 ovoliunlem1 24431 undmrnresiss 40936 |
Copyright terms: Public domain | W3C validator |