# Metamath Proof Explorer

## Theorem prneimg

Description: Two pairs are not equal if at least one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017)

Ref Expression
Assertion prneimg ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left(\left({A}\ne {C}\wedge {A}\ne {D}\right)\vee \left({B}\ne {C}\wedge {B}\ne {D}\right)\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}\right)$

### Proof

Step Hyp Ref Expression
1 preq12bg ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)\right)$
2 orddi ${⊢}\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)↔\left(\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({A}={C}\vee {B}={C}\right)\right)\wedge \left(\left({B}={D}\vee {A}={D}\right)\wedge \left({B}={D}\vee {B}={C}\right)\right)\right)$
3 simpll ${⊢}\left(\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({A}={C}\vee {B}={C}\right)\right)\wedge \left(\left({B}={D}\vee {A}={D}\right)\wedge \left({B}={D}\vee {B}={C}\right)\right)\right)\to \left({A}={C}\vee {A}={D}\right)$
4 pm1.4 ${⊢}\left({B}={D}\vee {B}={C}\right)\to \left({B}={C}\vee {B}={D}\right)$
5 4 ad2antll ${⊢}\left(\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({A}={C}\vee {B}={C}\right)\right)\wedge \left(\left({B}={D}\vee {A}={D}\right)\wedge \left({B}={D}\vee {B}={C}\right)\right)\right)\to \left({B}={C}\vee {B}={D}\right)$
6 3 5 jca ${⊢}\left(\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({A}={C}\vee {B}={C}\right)\right)\wedge \left(\left({B}={D}\vee {A}={D}\right)\wedge \left({B}={D}\vee {B}={C}\right)\right)\right)\to \left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)$
7 2 6 sylbi ${⊢}\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)\to \left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)$
8 1 7 syl6bi ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)\right)$
9 ianor ${⊢}¬\left({A}\ne {C}\wedge {A}\ne {D}\right)↔\left(¬{A}\ne {C}\vee ¬{A}\ne {D}\right)$
10 nne ${⊢}¬{A}\ne {C}↔{A}={C}$
11 nne ${⊢}¬{A}\ne {D}↔{A}={D}$
12 10 11 orbi12i ${⊢}\left(¬{A}\ne {C}\vee ¬{A}\ne {D}\right)↔\left({A}={C}\vee {A}={D}\right)$
13 9 12 bitr2i ${⊢}\left({A}={C}\vee {A}={D}\right)↔¬\left({A}\ne {C}\wedge {A}\ne {D}\right)$
14 ianor ${⊢}¬\left({B}\ne {C}\wedge {B}\ne {D}\right)↔\left(¬{B}\ne {C}\vee ¬{B}\ne {D}\right)$
15 nne ${⊢}¬{B}\ne {C}↔{B}={C}$
16 nne ${⊢}¬{B}\ne {D}↔{B}={D}$
17 15 16 orbi12i ${⊢}\left(¬{B}\ne {C}\vee ¬{B}\ne {D}\right)↔\left({B}={C}\vee {B}={D}\right)$
18 14 17 bitr2i ${⊢}\left({B}={C}\vee {B}={D}\right)↔¬\left({B}\ne {C}\wedge {B}\ne {D}\right)$
19 13 18 anbi12i ${⊢}\left(\left({A}={C}\vee {A}={D}\right)\wedge \left({B}={C}\vee {B}={D}\right)\right)↔\left(¬\left({A}\ne {C}\wedge {A}\ne {D}\right)\wedge ¬\left({B}\ne {C}\wedge {B}\ne {D}\right)\right)$
20 8 19 syl6ib ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left(¬\left({A}\ne {C}\wedge {A}\ne {D}\right)\wedge ¬\left({B}\ne {C}\wedge {B}\ne {D}\right)\right)\right)$
21 pm4.56 ${⊢}\left(¬\left({A}\ne {C}\wedge {A}\ne {D}\right)\wedge ¬\left({B}\ne {C}\wedge {B}\ne {D}\right)\right)↔¬\left(\left({A}\ne {C}\wedge {A}\ne {D}\right)\vee \left({B}\ne {C}\wedge {B}\ne {D}\right)\right)$
22 20 21 syl6ib ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to ¬\left(\left({A}\ne {C}\wedge {A}\ne {D}\right)\vee \left({B}\ne {C}\wedge {B}\ne {D}\right)\right)\right)$
23 22 necon2ad ${⊢}\left(\left({A}\in {U}\wedge {B}\in {V}\right)\wedge \left({C}\in {X}\wedge {D}\in {Y}\right)\right)\to \left(\left(\left({A}\ne {C}\wedge {A}\ne {D}\right)\vee \left({B}\ne {C}\wedge {B}\ne {D}\right)\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}\right)$