Metamath Proof Explorer


Theorem bj-rexcom4b

Description: Remove from rexcom4b dependency on ax-ext and ax-13 (and on df-or , df-cleq , df-nfc , df-v ). The hypothesis uses V instead of _V (see bj-isseti for the motivation). Use bj-rexcom4bv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

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

Proof

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