|   | 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 1847 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | 
| 3 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
| 4 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1778 ∈ wcel 2107 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-ex 1779 df-rex 3070 | 
| This theorem is referenced by: rexbiia 3091 rexeqbii 3344 rexrab 3701 rexin 4249 rexdifpr 4658 rexdifsn 4793 reusv2lem4 5400 reusv2 5402 frpoind 6362 wfiOLD 6371 eldifsucnn 8703 frind 9791 rexuz2 12942 rexrp 13057 rexuz3 15388 infpn2 16952 efgrelexlemb 19769 cmpcov2 23399 cmpfi 23417 txkgen 23661 cubic 26893 madeval2 27893 sumdmdii 32435 bnj882 34941 bnj893 34943 heibor1 37818 eldmqsres 38289 prtlem100 38861 islmodfg 43086 iuneq1i 45095 limcrecl 45649 | 
| Copyright terms: Public domain | W3C validator |