![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breq12i | Structured version Visualization version GIF version |
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
breq1i.1 | ⊢ 𝐴 = 𝐵 |
breq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
breq12i | ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | breq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | breq12 5153 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷)) | |
4 | 1, 2, 3 | mp2an 689 | 1 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1540 class class class wbr 5148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-br 5149 |
This theorem is referenced by: 3brtr3g 5181 3brtr4g 5182 caovord2 7623 domunfican 9326 ltsonq 10970 ltanq 10972 ltmnq 10973 prlem934 11034 prlem936 11048 ltsosr 11095 ltasr 11101 ltneg 11721 leneg 11724 inelr 12209 lt2sqi 14160 le2sqi 14161 nn0le2msqi 14234 2sqreuop 27307 2sqreuopnn 27308 2sqreuoplt 27309 2sqreuopltb 27310 2sqreuopnnlt 27311 2sqreuopnnltb 27312 axlowdimlem6 28637 upgrwlkcompim 29332 clwlkcompbp 29471 mdsldmd1i 32016 divcnvlin 35171 relowlpssretop 36708 2ap1caineq 41427 fsumlessf 44751 climlimsupcex 44943 liminfltlimsupex 44955 liminflelimsupcex 44971 sge0xaddlem2 45608 eubrdm 46204 iscmgmALT 47060 iscsgrpALT 47062 |
Copyright terms: Public domain | W3C validator |