Metamath Proof Explorer

Theorem brfvidRP

Description: If two elements are connected by a value of the identity relation, then they are connected via the argument. This is an example which uses brmptiunrelexpd . (Contributed by RP, 21-Jul-2020) (Proof modification is discouraged.)

Ref Expression
Hypothesis brfvidRP.r ⊢ φ → R ∈ V
Assertion brfvidRP ⊢ φ → A I ⁡ R B ↔ A R B

Proof

Step Hyp Ref Expression
1 brfvidRP.r ⊢ φ → R ∈ V
2 dfid6 ⊢ I = r ∈ V ⟼ ⋃ n ∈ 1 r ↑ r n
3 1nn0 ⊢ 1 ∈ ℕ 0
4 snssi ⊢ 1 ∈ ℕ 0 → 1 ⊆ ℕ 0
5 3 4 mp1i ⊢ φ → 1 ⊆ ℕ 0
6 2 1 5 brmptiunrelexpd ⊢ φ → A I ⁡ R B ↔ ∃ n ∈ 1 A R ↑ r n B
7 oveq2 ⊢ n = 1 → R ↑ r n = R ↑ r 1
8 7 breqd ⊢ n = 1 → A R ↑ r n B ↔ A R ↑ r 1 B
9 8 rexsng ⊢ 1 ∈ ℕ 0 → ∃ n ∈ 1 A R ↑ r n B ↔ A R ↑ r 1 B
10 3 9 mp1i ⊢ φ → ∃ n ∈ 1 A R ↑ r n B ↔ A R ↑ r 1 B
11 1 relexp1d ⊢ φ → R ↑ r 1 = R
12 11 breqd ⊢ φ → A R ↑ r 1 B ↔ A R B
13 6 10 12 3bitrd ⊢ φ → A I ⁡ R B ↔ A R B