![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rexbii2 | Structured version Visualization version GIF version |
Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.) |
Ref | Expression |
---|---|
rexbii2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) |
Ref | Expression |
---|---|
rexbii2 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbii2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓)) | |
2 | 1 | exbii 1923 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3056 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3056 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∃wex 1853 ∈ wcel 2139 ∃wrex 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 |
This theorem depends on definitions: df-bi 197 df-ex 1854 df-rex 3056 |
This theorem is referenced by: rexbiia 3178 rexbii 3179 rexeqbii 3192 rexrab 3511 rexdifpr 4350 rexdifsn 4469 reusv2lem4 5021 reusv2 5023 wefrc 5260 wfi 5874 bnd2 8929 rexuz2 11932 rexrp 12046 rexuz3 14287 infpn2 15819 efgrelexlemb 18363 cmpcov2 21395 cmpfi 21413 subislly 21486 txkgen 21657 cubic 24775 sumdmdii 29583 pcmplfin 30236 bnj882 31303 bnj893 31305 imaindm 31987 frpoind 32046 frind 32049 madeval2 32242 heibor1 33922 eldmqsres 34375 prtlem100 34648 islmodfg 38141 limcrecl 40364 |
Copyright terms: Public domain | W3C validator |