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

Metamath Proof Explorer

Theorem elmptrab2

Description: Membership in a one-parameter class of sets, indexed by arbitrary base sets. (Contributed by Stefan O'Rear, 28-Jul-2015) (Revised by AV, 26-Mar-2021)

		Ref	Expression
	Hypotheses	elmptrab2.f	$⊢ F = (x \in V ⟼ \{y \in B \| φ\})$
		elmptrab2.s1	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
		elmptrab2.s2	$⊢ x = X \to B = C$
		elmptrab2.ex	$⊢ B \in V$
		elmptrab2.rc	$⊢ Y \in C \to X \in W$
	Assertion	elmptrab2	$⊢ Y \in F (X) \leftrightarrow (Y \in C \land ψ)$

Proof

Step	Hyp	Ref	Expression
1		elmptrab2.f	$⊢ F = (x \in V ⟼ \{y \in B \| φ\})$
2		elmptrab2.s1	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow ψ)$
3		elmptrab2.s2	$⊢ x = X \to B = C$
4		elmptrab2.ex	$⊢ B \in V$
5		elmptrab2.rc	$⊢ Y \in C \to X \in W$
6	4	a1i	$⊢ x \in V \to B \in V$
7	1 2 3 6	elmptrab	$⊢ Y \in F (X) \leftrightarrow (X \in V \land Y \in C \land ψ)$
8		3simpc	$⊢ (X \in V \land Y \in C \land ψ) \to (Y \in C \land ψ)$
9	5	elexd	$⊢ Y \in C \to X \in V$
10	9	adantr	$⊢ (Y \in C \land ψ) \to X \in V$
11		simpl	$⊢ (Y \in C \land ψ) \to Y \in C$
12		simpr	$⊢ (Y \in C \land ψ) \to ψ$
13	10 11 12	3jca	$⊢ (Y \in C \land ψ) \to (X \in V \land Y \in C \land ψ)$
14	8 13	impbii	$⊢ (X \in V \land Y \in C \land ψ) \leftrightarrow (Y \in C \land ψ)$
15	7 14	bitri	$⊢ Y \in F (X) \leftrightarrow (Y \in C \land ψ)$