This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ineccnvmo

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 2-Sep-2021)

Ref Expression
Assertion ineccnvmo 
|- ( A. y e. B A. z e. B ( y = z \/ ( [ y ] `' F i^i [ z ] `' F ) = (/) ) <-> A. x E* y e. B x F y )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' F
2 id 
 |-  ( y = z -> y = z )
3 2 inecmo 
 |-  ( Rel `' F -> ( A. y e. B A. z e. B ( y = z \/ ( [ y ] `' F i^i [ z ] `' F ) = (/) ) <-> A. x E* y e. B y `' F x ) )
4 1 3 ax-mp 
 |-  ( A. y e. B A. z e. B ( y = z \/ ( [ y ] `' F i^i [ z ] `' F ) = (/) ) <-> A. x E* y e. B y `' F x )
5 brcnvg 
 |-  ( ( y e. _V /\ x e. _V ) -> ( y `' F x <-> x F y ) )
6 5 el2v 
 |-  ( y `' F x <-> x F y )
7 6 rmobii 
 |-  ( E* y e. B y `' F x <-> E* y e. B x F y )
8 7 albii 
 |-  ( A. x E* y e. B y `' F x <-> A. x E* y e. B x F y )
9 4 8 bitri 
 |-  ( A. y e. B A. z e. B ( y = z \/ ( [ y ] `' F i^i [ z ] `' F ) = (/) ) <-> A. x E* y e. B x F y )