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

Metamath Proof Explorer

Theorem gencl

Description: Implicit substitution for class with embedded variable. (Contributed by NM, 17-May-1996)

Ref Expression
Hypotheses gencl.1 ⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝐵 ) )
gencl.2 ⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
gencl.3 ⊢ ( 𝜒 → 𝜑 )
Assertion gencl ( 𝜃 → 𝜓 )

Proof

Step Hyp Ref Expression
1 gencl.1 ⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝐵 ) )
2 gencl.2 ⊢ ( 𝐴 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
3 gencl.3 ⊢ ( 𝜒 → 𝜑 )
4 3 2 imbitrid ⊢ ( 𝐴 = 𝐵 → ( 𝜒 → 𝜓 ) )
5 4 impcom ⊢ ( ( 𝜒 ∧ 𝐴 = 𝐵 ) → 𝜓 )
6 5 exlimiv ⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝐵 ) → 𝜓 )
7 1 6 sylbi ⊢ ( 𝜃 → 𝜓 )