Metamath Proof Explorer


Theorem bj-rexcom4bv

Description: Version of rexcom4b and bj-rexcom4b with a disjoint variable condition on x , V , hence removing dependency on df-sb and df-clab (so that it depends on df-clel and df-rex only on top of first-order logic). Prefer its use over bj-rexcom4b when sufficient (in particular when V is substituted for _V ). Note the V in the hypothesis instead of _V . (Contributed by BJ, 14-Sep-2019) (Proof modification is discouraged.)

Ref Expression
Hypothesis bj-rexcom4bv.1 𝐵𝑉
Assertion bj-rexcom4bv ( ∃ 𝑥𝑦𝐴 ( 𝜑𝑥 = 𝐵 ) ↔ ∃ 𝑦𝐴 𝜑 )

Proof

Step Hyp Ref Expression
1 bj-rexcom4bv.1 𝐵𝑉
2 rexcom4a ( ∃ 𝑥𝑦𝐴 ( 𝜑𝑥 = 𝐵 ) ↔ ∃ 𝑦𝐴 ( 𝜑 ∧ ∃ 𝑥 𝑥 = 𝐵 ) )
3 1 bj-issetiv 𝑥 𝑥 = 𝐵
4 3 biantru ( 𝜑 ↔ ( 𝜑 ∧ ∃ 𝑥 𝑥 = 𝐵 ) )
5 4 rexbii ( ∃ 𝑦𝐴 𝜑 ↔ ∃ 𝑦𝐴 ( 𝜑 ∧ ∃ 𝑥 𝑥 = 𝐵 ) )
6 2 5 bitr4i ( ∃ 𝑥𝑦𝐴 ( 𝜑𝑥 = 𝐵 ) ↔ ∃ 𝑦𝐴 𝜑 )