![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ndmovrcl | Structured version Visualization version GIF version |
Description: Reverse closure law, when an operation's domain doesn't contain the empty set. (Contributed by NM, 3-Feb-1996.) |
Ref | Expression |
---|---|
ndmov.1 | ⊢ dom 𝐹 = (𝑆 × 𝑆) |
ndmovrcl.3 | ⊢ ¬ ∅ ∈ 𝑆 |
Ref | Expression |
---|---|
ndmovrcl | ⊢ ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ndmovrcl.3 | . . 3 ⊢ ¬ ∅ ∈ 𝑆 | |
2 | ndmov.1 | . . . . 5 ⊢ dom 𝐹 = (𝑆 × 𝑆) | |
3 | 2 | ndmov 7148 | . . . 4 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) = ∅) |
4 | 3 | eleq1d 2850 | . . 3 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ((𝐴𝐹𝐵) ∈ 𝑆 ↔ ∅ ∈ 𝑆)) |
5 | 1, 4 | mtbiri 319 | . 2 ⊢ (¬ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ¬ (𝐴𝐹𝐵) ∈ 𝑆) |
6 | 5 | con4i 114 | 1 ⊢ ((𝐴𝐹𝐵) ∈ 𝑆 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ∅c0 4178 × cxp 5405 dom cdm 5407 (class class class)co 6976 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-xp 5413 df-dm 5417 df-iota 6152 df-fv 6196 df-ov 6979 |
This theorem is referenced by: ndmovass 7152 ndmovdistr 7153 ndmovord 7154 ndmovordi 7155 caovmo 7201 brecop2 8191 eceqoveq 8202 addcanpi 10119 mulcanpi 10120 ordpipq 10162 recmulnq 10184 recclnq 10186 ltexnq 10195 nsmallnq 10197 ltbtwnnq 10198 prlem934 10253 ltaddpr 10254 ltaddpr2 10255 ltexprlem2 10257 ltexprlem3 10258 ltexprlem4 10259 ltexprlem6 10261 ltexprlem7 10262 addcanpr 10266 prlem936 10267 mappsrpr 10328 |
Copyright terms: Public domain | W3C validator |