Metamath Proof Explorer


Theorem elunirn2OLD

Description: Obsolete version of elfvunirn as of 12-Jan-2025. (Contributed by Thierry Arnoux, 13-Nov-2016) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion elunirn2OLD ( ( Fun 𝐹𝐵 ∈ ( 𝐹𝐴 ) ) → 𝐵 ran 𝐹 )

Proof

Step Hyp Ref Expression
1 elfvdm ( 𝐵 ∈ ( 𝐹𝐴 ) → 𝐴 ∈ dom 𝐹 )
2 fveq2 ( 𝑥 = 𝐴 → ( 𝐹𝑥 ) = ( 𝐹𝐴 ) )
3 2 eleq2d ( 𝑥 = 𝐴 → ( 𝐵 ∈ ( 𝐹𝑥 ) ↔ 𝐵 ∈ ( 𝐹𝐴 ) ) )
4 3 rspcev ( ( 𝐴 ∈ dom 𝐹𝐵 ∈ ( 𝐹𝐴 ) ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹𝑥 ) )
5 1 4 mpancom ( 𝐵 ∈ ( 𝐹𝐴 ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹𝑥 ) )
6 5 adantl ( ( Fun 𝐹𝐵 ∈ ( 𝐹𝐴 ) ) → ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹𝑥 ) )
7 elunirn ( Fun 𝐹 → ( 𝐵 ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹𝑥 ) ) )
8 7 adantr ( ( Fun 𝐹𝐵 ∈ ( 𝐹𝐴 ) ) → ( 𝐵 ran 𝐹 ↔ ∃ 𝑥 ∈ dom 𝐹 𝐵 ∈ ( 𝐹𝑥 ) ) )
9 6 8 mpbird ( ( Fun 𝐹𝐵 ∈ ( 𝐹𝐴 ) ) → 𝐵 ran 𝐹 )