Metamath Proof Explorer


Theorem ocel

Description: Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000) (New usage is discouraged.)

Ref Expression
Assertion ocel H A H A x H A ih x = 0

Proof

Step Hyp Ref Expression
1 ocval H H = y | x H y ih x = 0
2 1 eleq2d H A H A y | x H y ih x = 0
3 oveq1 y = A y ih x = A ih x
4 3 eqeq1d y = A y ih x = 0 A ih x = 0
5 4 ralbidv y = A x H y ih x = 0 x H A ih x = 0
6 5 elrab A y | x H y ih x = 0 A x H A ih x = 0
7 2 6 bitrdi H A H A x H A ih x = 0