Metamath Proof Explorer

Theorem isowe2

Description: A weak form of isowe that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion isowe2 ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → S We B → R We A

Proof

Step Hyp Ref Expression
1 simpl ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → H Isom R , S A B
2 imaeq2 ⊢ x = y → H x = H y
3 2 eleq1d ⊢ x = y → H x ∈ V ↔ H y ∈ V
4 3 spvv ⊢ ∀ x H x ∈ V → H y ∈ V
5 4 adantl ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → H y ∈ V
6 1 5 isofrlem ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → S Fr B → R Fr A
7 isosolem ⊢ H Isom R , S A B → S Or B → R Or A
8 7 adantr ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → S Or B → R Or A
9 6 8 anim12d ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → S Fr B ∧ S Or B → R Fr A ∧ R Or A
10 df-we ⊢ S We B ↔ S Fr B ∧ S Or B
11 df-we ⊢ R We A ↔ R Fr A ∧ R Or A
12 9 10 11 3imtr4g ⊢ H Isom R , S A B ∧ ∀ x H x ∈ V → S We B → R We A