Metamath Proof Explorer


Theorem reuun2

Description: Transfer uniqueness to a smaller or larger class. (Contributed by NM, 21-Oct-2005)

Ref Expression
Assertion reuun2 ( ¬ ∃ 𝑥𝐵 𝜑 → ( ∃! 𝑥 ∈ ( 𝐴𝐵 ) 𝜑 ↔ ∃! 𝑥𝐴 𝜑 ) )

Proof

Step Hyp Ref Expression
1 df-rex ( ∃ 𝑥𝐵 𝜑 ↔ ∃ 𝑥 ( 𝑥𝐵𝜑 ) )
2 euor2 ( ¬ ∃ 𝑥 ( 𝑥𝐵𝜑 ) → ( ∃! 𝑥 ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) ↔ ∃! 𝑥 ( 𝑥𝐴𝜑 ) ) )
3 1 2 sylnbi ( ¬ ∃ 𝑥𝐵 𝜑 → ( ∃! 𝑥 ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) ↔ ∃! 𝑥 ( 𝑥𝐴𝜑 ) ) )
4 df-reu ( ∃! 𝑥 ∈ ( 𝐴𝐵 ) 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ 𝜑 ) )
5 elun ( 𝑥 ∈ ( 𝐴𝐵 ) ↔ ( 𝑥𝐴𝑥𝐵 ) )
6 5 anbi1i ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐴𝑥𝐵 ) ∧ 𝜑 ) )
7 andir ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐴𝜑 ) ∨ ( 𝑥𝐵𝜑 ) ) )
8 orcom ( ( ( 𝑥𝐴𝜑 ) ∨ ( 𝑥𝐵𝜑 ) ) ↔ ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) )
9 7 8 bitri ( ( ( 𝑥𝐴𝑥𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) )
10 6 9 bitri ( ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ 𝜑 ) ↔ ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) )
11 10 eubii ( ∃! 𝑥 ( 𝑥 ∈ ( 𝐴𝐵 ) ∧ 𝜑 ) ↔ ∃! 𝑥 ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) )
12 4 11 bitri ( ∃! 𝑥 ∈ ( 𝐴𝐵 ) 𝜑 ↔ ∃! 𝑥 ( ( 𝑥𝐵𝜑 ) ∨ ( 𝑥𝐴𝜑 ) ) )
13 df-reu ( ∃! 𝑥𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥𝐴𝜑 ) )
14 3 12 13 3bitr4g ( ¬ ∃ 𝑥𝐵 𝜑 → ( ∃! 𝑥 ∈ ( 𝐴𝐵 ) 𝜑 ↔ ∃! 𝑥𝐴 𝜑 ) )