Step |
Hyp |
Ref |
Expression |
1 |
|
mpoxeldm.f |
|- F = ( x e. C , y e. D |-> R ) |
2 |
|
df-nel |
|- ( X e/ C <-> -. X e. C ) |
3 |
|
df-nel |
|- ( Y e/ [_ X / x ]_ D <-> -. Y e. [_ X / x ]_ D ) |
4 |
2 3
|
orbi12i |
|- ( ( X e/ C \/ Y e/ [_ X / x ]_ D ) <-> ( -. X e. C \/ -. Y e. [_ X / x ]_ D ) ) |
5 |
|
ianor |
|- ( -. ( X e. C /\ Y e. [_ X / x ]_ D ) <-> ( -. X e. C \/ -. Y e. [_ X / x ]_ D ) ) |
6 |
4 5
|
bitr4i |
|- ( ( X e/ C \/ Y e/ [_ X / x ]_ D ) <-> -. ( X e. C /\ Y e. [_ X / x ]_ D ) ) |
7 |
|
neq0 |
|- ( -. ( X F Y ) = (/) <-> E. n n e. ( X F Y ) ) |
8 |
1
|
mpoxeldm |
|- ( n e. ( X F Y ) -> ( X e. C /\ Y e. [_ X / x ]_ D ) ) |
9 |
8
|
exlimiv |
|- ( E. n n e. ( X F Y ) -> ( X e. C /\ Y e. [_ X / x ]_ D ) ) |
10 |
7 9
|
sylbi |
|- ( -. ( X F Y ) = (/) -> ( X e. C /\ Y e. [_ X / x ]_ D ) ) |
11 |
10
|
con1i |
|- ( -. ( X e. C /\ Y e. [_ X / x ]_ D ) -> ( X F Y ) = (/) ) |
12 |
6 11
|
sylbi |
|- ( ( X e/ C \/ Y e/ [_ X / x ]_ D ) -> ( X F Y ) = (/) ) |