Metamath Proof Explorer


Theorem rexima

Description: Existential quantification under an image in terms of the base set. (Contributed by Stefan O'Rear, 21-Jan-2015) Reduce DV conditions. (Revised by Matthew House, 14-Aug-2025)

Ref Expression
Hypothesis ralima.x ( 𝑥 = ( 𝐹𝑦 ) → ( 𝜑𝜓 ) )
Assertion rexima ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ∃ 𝑦𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ralima.x ( 𝑥 = ( 𝐹𝑦 ) → ( 𝜑𝜓 ) )
2 1 notbid ( 𝑥 = ( 𝐹𝑦 ) → ( ¬ 𝜑 ↔ ¬ 𝜓 ) )
3 2 ralima ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∀ 𝑥 ∈ ( 𝐹𝐵 ) ¬ 𝜑 ↔ ∀ 𝑦𝐵 ¬ 𝜓 ) )
4 3 notbid ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ¬ ∀ 𝑥 ∈ ( 𝐹𝐵 ) ¬ 𝜑 ↔ ¬ ∀ 𝑦𝐵 ¬ 𝜓 ) )
5 dfrex2 ( ∃ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ¬ ∀ 𝑥 ∈ ( 𝐹𝐵 ) ¬ 𝜑 )
6 dfrex2 ( ∃ 𝑦𝐵 𝜓 ↔ ¬ ∀ 𝑦𝐵 ¬ 𝜓 )
7 4 5 6 3bitr4g ( ( 𝐹 Fn 𝐴𝐵𝐴 ) → ( ∃ 𝑥 ∈ ( 𝐹𝐵 ) 𝜑 ↔ ∃ 𝑦𝐵 𝜓 ) )