Metamath Proof Explorer


Theorem spcimgfi1OLD

Description: Obsolete version of spcimgfi1 as of 27-Jul-2025. (Contributed by Mario Carneiro, 4-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses spcimgfi1.1 𝑥 𝜓
spcimgfi1.2 𝑥 𝐴
Assertion spcimgfi1OLD ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝐴𝐵 → ( ∀ 𝑥 𝜑𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 spcimgfi1.1 𝑥 𝜓
2 spcimgfi1.2 𝑥 𝐴
3 elex ( 𝐴𝐵𝐴 ∈ V )
4 2 issetf ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
5 exim ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( 𝜑𝜓 ) ) )
6 4 5 biimtrid ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝐴 ∈ V → ∃ 𝑥 ( 𝜑𝜓 ) ) )
7 1 19.36 ( ∃ 𝑥 ( 𝜑𝜓 ) ↔ ( ∀ 𝑥 𝜑𝜓 ) )
8 6 7 imbitrdi ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝐴 ∈ V → ( ∀ 𝑥 𝜑𝜓 ) ) )
9 3 8 syl5 ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝐴𝐵 → ( ∀ 𝑥 𝜑𝜓 ) ) )